src/Tools/induct.ML

 (* mark equality constraints in cases rule *)
 
 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
   (Raw_Simplifier.rewrite true [Induct_Args.equal_def]);
 

         let val rule' =
           (if simp then simplified_rule' ctxt #> unmark_constraints else I) rule
         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;
 
 end;

   |> filter_out (forall Rule_Cases.is_inner_rule);
 
 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
     val thy = Proof_Context.theory_of ctxt;
 

 
     fun rule_cases ctxt rule cases =
       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
       |> Seq.maps (Rule_Cases.consume (flat defs) facts)
       |> Seq.maps (fn (((cases, concls), (more_consumes, more_facts)), rule) =>
         (PRECISE_CONJUNCTS (length concls) (ALLGOALS (fn j =>
           (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)
           THEN' inner_atomize_tac) j))
         THEN' atomize_tac) i st |> Seq.maps (fn st' =>
             guess_instance ctxt (internalize more_consumes rule) i st'
             |> 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)
         else K all_tac)
        THEN_ALL_NEW rulify_tac)
   end;
 
 val induct_tac = gen_induct_tac (K I);
+
+
 
 (** coinduct method **)
 
 (*
   rule selection scheme:

         guess_instance ctxt rule i st
         |> Seq.map (rule_instance ctxt (burrow_options (Variable.polymorphic ctxt) taking))
         |> 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;