src/Tools/induct.ML
changeset 24832 64cd13299d39
parent 24830 a7b3ab44d993
child 24861 cc669ca5f382
--- a/src/Tools/induct.ML	Thu Oct 04 16:21:31 2007 +0200
+++ b/src/Tools/induct.ML	Thu Oct 04 16:59:28 2007 +0200
@@ -522,15 +522,15 @@
     | NONE => all_tac)
   end);
 
-fun miniscope_tac p =
-  CONVERSION (Conv.forall_conv p (MetaSimplifier.rewrite true [Thm.symmetric Drule.norm_hhf_eq]));
+fun miniscope_tac p = CONVERSION o
+  Conv.forall_conv p (K (MetaSimplifier.rewrite true [Thm.symmetric Drule.norm_hhf_eq]));
 
 in
 
 fun fix_tac _ _ [] = K all_tac
   | fix_tac ctxt n xs = SUBGOAL (fn (goal, i) =>
      (EVERY' (map (meta_spec_tac ctxt n) xs) THEN'
-      (miniscope_tac (goal_params n goal))) i);
+      (miniscope_tac (goal_params n goal) ctxt)) i);
 
 end;