src/Pure/subgoal.ML
changeset 59058 a78612c67ec0
parent 58950 d07464875dd4
child 59573 d09cc83cdce9
     1.1 --- a/src/Pure/subgoal.ML	Wed Nov 26 16:55:43 2014 +0100
     1.2 +++ b/src/Pure/subgoal.ML	Wed Nov 26 20:05:34 2014 +0100
     1.3 @@ -86,7 +86,7 @@
     1.4            else (Ts ---> T, ts);
     1.5          val u = Free (y, U);
     1.6          in ((Var v, list_comb (u, args)), (u, Var ((x, i + idx), U))) end;
     1.7 -    val (inst1, inst2) = split_list (map (pairself (pairself cert)) (map2 var_inst vars ys));
     1.8 +    val (inst1, inst2) = split_list (map (apply2 (apply2 cert)) (map2 var_inst vars ys));
     1.9  
    1.10      val th'' = Thm.instantiate ([], inst1) th';
    1.11    in ((inst2, th''), ctxt'') end;