# HG changeset patch
# User wenzelm
# Date 1318445860 -7200
# Node ID 563caf031b506fec21851e02b5976e68571fe82e
# Parent  1fce03e3e8ad1cff74015579405229cda77dbd68
tuned ML style;

diff -r 1fce03e3e8ad -r 563caf031b50 src/Tools/induct.ML
--- a/src/Tools/induct.ML	Wed Oct 12 20:16:48 2011 +0200
+++ b/src/Tools/induct.ML	Wed Oct 12 20:57:40 2011 +0200
@@ -429,7 +429,7 @@
 val equal_def' = Thm.symmetric Induct_Args.equal_def;
 
 fun mark_constraints n ctxt = Conv.fconv_rule
-  (Conv.prems_conv (~1) (Conv.params_conv ~1 (K (Conv.prems_conv n
+  (Conv.prems_conv ~1 (Conv.params_conv ~1 (K (Conv.prems_conv n
      (Raw_Simplifier.rewrite false [equal_def']))) ctxt));
 
 val unmark_constraints = Conv.fconv_rule
@@ -507,7 +507,7 @@
         in
           CASES (Rule_Cases.make_common (thy,
               Thm.prop_of (Rule_Cases.internalize_params rule')) cases)
-            ((Method.insert_tac more_facts THEN' Tactic.rtac rule' THEN_ALL_NEW
+            ((Method.insert_tac more_facts THEN' rtac rule' THEN_ALL_NEW
                 (if simp then TRY o trivial_tac else K all_tac)) i) st
         end)
   end;
@@ -731,7 +731,7 @@
 fun get_inductP ctxt (fact :: _) = map single (find_inductP ctxt (Thm.concl_of fact))
   | get_inductP _ _ = [];
 
-type case_data = (((string * string list) * string list) list * int)
+type case_data = (((string * string list) * string list) list * int);
 
 fun gen_induct_tac mod_cases ctxt simp def_insts arbitrary taking opt_rule facts =
   let
@@ -763,12 +763,9 @@
       let
         val rule' = Rule_Cases.internalize_params rule;
         val rule'' = (if simp then simplified_rule ctxt else I) rule';
-        val nonames = map (fn ((cn,_),cls) => ((cn,[]),cls))
-        val cases' =
-          if Thm.eq_thm_prop (rule', rule'') then cases else nonames cases
-      in Rule_Cases.make_nested (Thm.prop_of rule'') (rulified_term rule'')
-           cases'
-      end;
+        val nonames = map (fn ((cn, _), cls) => ((cn, []), cls));
+        val cases' = if Thm.eq_thm_prop (rule', rule'') then cases else nonames cases;
+      in Rule_Cases.make_nested (Thm.prop_of rule'') (rulified_term rule'') cases' end;
   in
     (fn i => fn st =>
       ruleq
@@ -778,15 +775,14 @@
           (CONJUNCTS (ALLGOALS
             let
               val adefs = nth_list atomized_defs (j - 1);
-              val frees = fold (Term.add_frees o prop_of) adefs [];
+              val frees = fold (Term.add_frees o Thm.prop_of) adefs [];
               val xs = nth_list arbitrary (j - 1);
               val k = nth concls (j - 1) + more_consumes
             in
               Method.insert_tac (more_facts @ adefs) THEN'
                 (if simp then
                    rotate_tac k (length adefs) THEN'
-                   fix_tac defs_ctxt k
-                     (List.partition (member op = frees) xs |> op @)
+                   fix_tac defs_ctxt k (List.partition (member op = frees) xs |> op @)
                  else
                    fix_tac defs_ctxt k xs)
              end)
@@ -796,7 +792,7 @@
             |> Seq.map (rule_instance ctxt (burrow_options (Variable.polymorphic ctxt) taking))
             |> Seq.maps (fn rule' =>
               CASES (rule_cases ctxt rule' cases)
-                (Tactic.rtac rule' i THEN
+                (rtac rule' i THEN
                   PRIMITIVE (singleton (Proof_Context.export defs_ctxt ctxt))) st'))))
     THEN_ALL_NEW_CASES
       ((if simp then simplify_tac ctxt THEN' (TRY o trivial_tac)
@@ -806,6 +802,8 @@
 
 val induct_tac = gen_induct_tac (K I);
 
+
+
 (** coinduct method **)
 
 (*
@@ -853,7 +851,7 @@
         |> Seq.maps (fn rule' =>
           CASES (Rule_Cases.make_common (thy,
               Thm.prop_of (Rule_Cases.internalize_params rule')) cases)
-            (Method.insert_tac more_facts i THEN Tactic.rtac rule' i) st)))
+            (Method.insert_tac more_facts i THEN rtac rule' i) st)))
   end;
 
 end;