diff -r b2e1a7b83e05 -r 67370521c09c Nominal/nominal_induct.ML --- a/Nominal/nominal_induct.ML Tue Jul 08 11:18:31 2014 +0100 +++ b/Nominal/nominal_induct.ML Thu Jul 09 02:32:46 2015 +0100 @@ -57,7 +57,7 @@ end; val substs = map2 subst insts concls |> flat |> distinct (op =) - |> map (pairself (Thm.cterm_of (Proof_Context.theory_of ctxt))); + |> map (apply2 (Thm.cterm_of ctxt)); in (((cases, nconcls), consumes), Drule.cterm_instantiate substs joined_rule) end; @@ -86,9 +86,6 @@ fun nominal_induct_tac ctxt simp def_insts avoiding fixings rules facts = let - val thy = Proof_Context.theory_of ctxt; - val cert = Thm.cterm_of thy; - val ((insts, defs), defs_ctxt) = fold_map Induct.add_defs def_insts ctxt |>> split_list; val atomized_defs = map (map (Conv.fconv_rule (Induct.atomize_cterm defs_ctxt))) defs; @@ -99,7 +96,7 @@ fun rule_cases ctxt r = let val r' = if simp then Induct.simplified_rule ctxt r else r - in Rule_Cases.make_nested (Thm.prop_of r') (Induct.rulified_term r') end; + in Rule_Cases.make_nested ctxt (Thm.prop_of r') (Induct.rulified_term ctxt r') end; in (fn i => fn st => rules @@ -110,7 +107,7 @@ (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 fixings (j - 1); val k = nth concls (j - 1) + more_consumes in @@ -131,7 +128,7 @@ (Tactic.rtac (rename_params_rule false [] rule') i THEN PRIMITIVE (singleton (Proof_Context.export defs_ctxt ctxt))) st')))) THEN_ALL_NEW_CASES - ((if simp then Induct.simplify_tac ctxt THEN' (TRY o Induct.trivial_tac) + ((if simp then Induct.simplify_tac ctxt THEN' (TRY o Induct.trivial_tac ctxt) else K all_tac) THEN_ALL_NEW Induct.rulify_tac ctxt) end; @@ -176,9 +173,8 @@ Scan.lift (Args.mode Induct.no_simpN) -- (Parse.and_list' (Scan.repeat (unless_more_args def_inst)) -- avoiding -- fixing -- rule_spec) >> - (fn (no_simp, (((x, y), z), w)) => fn ctxt => - RAW_METHOD_CASES (fn facts => - HEADGOAL (nominal_induct_tac ctxt (not no_simp) x y z w facts))); + (fn (no_simp, (((x, y), z), w)) => fn ctxt => fn facts => + HEADGOAL (nominal_induct_tac ctxt (not no_simp) x y z w facts)); end