Lines Matching defs:arg2
48 | APP(loc1, APP(loc2, IDENT (loc3, ","), arg1), arg2) =>
49 VPAIR(loc1, to_vstruct arg1, to_vstruct arg2)
65 APP(loc1, APP(loc2, IDENT(loc3, s), arg1), arg2) => let
68 (to_vstruct arg1, arg2)
71 val (v2,a2) = clean_action arg2
85 APP(loc1, APP(loc2, IDENT(loc3, s), arg1), arg2) => let
89 val arg2' = clean_actions arg2
91 case arg2' of
114 APP(l,arg1 as APP(_,IDENT(_,s),_),arg2) =>
118 else APP(l,clean_do arg1,clean_do arg2)
176 val (arg1, arg2) = valOf (dest_bind tmg t)
234 fun brk_bind arg1 arg2 = let
235 val (v,body) = (SOME ## I) (pairSyntax.dest_pabs arg2)
236 handle HOL_ERR _ => (NONE, arg2)
243 | SOME (arg1, arg2) => let
244 val (arg1', arg2') = brk_bind arg1 arg2
246 strip (arg1'::acc) arg2'
248 val (arg1',arg2') = brk_bind arg1 arg2
249 val actions = strip [arg1'] arg2'