1.1 --- a/src/Tools/induct.ML	Fri Dec 13 23:53:02 2013 +0100
     1.2 +++ b/src/Tools/induct.ML	Sat Dec 14 17:28:05 2013 +0100
     1.3 @@ -60,16 +60,16 @@
     1.4    val add_defs: (binding option * (term * bool)) option list -> Proof.context ->
     1.5      (term option list * thm list) * Proof.context
     1.6    val atomize_term: theory -> term -> term
     1.7 -  val atomize_cterm: conv
     1.8 -  val atomize_tac: int -> tactic
     1.9 -  val inner_atomize_tac: int -> tactic
    1.10 +  val atomize_cterm: Proof.context -> conv
    1.11 +  val atomize_tac: Proof.context -> int -> tactic
    1.12 +  val inner_atomize_tac: Proof.context -> int -> tactic
    1.13    val rulified_term: thm -> theory * term
    1.14 -  val rulify_tac: int -> tactic
    1.15 +  val rulify_tac: Proof.context -> int -> tactic
    1.16    val simplified_rule: Proof.context -> thm -> thm
    1.17    val simplify_tac: Proof.context -> int -> tactic
    1.18    val trivial_tac: int -> tactic
    1.19    val rotate_tac: int -> int -> int -> tactic
    1.20 -  val internalize: int -> thm -> thm
    1.21 +  val internalize: Proof.context -> int -> thm -> thm
    1.22    val guess_instance: Proof.context -> thm -> int -> thm -> thm Seq.seq
    1.23    val cases_tac: Proof.context -> bool -> term option list list -> thm option ->
    1.24      thm list -> int -> cases_tactic
    1.25 @@ -433,10 +433,10 @@
    1.26  
    1.27  fun mark_constraints n ctxt = Conv.fconv_rule
    1.28    (Conv.prems_conv ~1 (Conv.params_conv ~1 (K (Conv.prems_conv n
    1.29 -     (Raw_Simplifier.rewrite false [equal_def']))) ctxt));
    1.30 +     (Raw_Simplifier.rewrite ctxt false [equal_def']))) ctxt));
    1.31  
    1.32 -val unmark_constraints = Conv.fconv_rule
    1.33 -  (Raw_Simplifier.rewrite true [Induct_Args.equal_def]);
    1.34 +fun unmark_constraints ctxt =
    1.35 +  Conv.fconv_rule (Raw_Simplifier.rewrite ctxt true [Induct_Args.equal_def]);
    1.36  
    1.37  
    1.38  (* simplify *)
    1.39 @@ -504,11 +504,11 @@
    1.40    in
    1.41      fn i => fn st =>
    1.42        ruleq
    1.43 -      |> Seq.maps (Rule_Cases.consume [] facts)
    1.44 +      |> Seq.maps (Rule_Cases.consume ctxt [] facts)
    1.45        |> Seq.maps (fn ((cases, (_, more_facts)), rule) =>
    1.46          let
    1.47            val rule' = rule
    1.48 -            |> simp ? (simplified_rule' ctxt #> unmark_constraints);
    1.49 +            |> simp ? (simplified_rule' ctxt #> unmark_constraints ctxt);
    1.50          in
    1.51            CASES (Rule_Cases.make_common (thy,
    1.52                Thm.prop_of (Rule_Cases.internalize_params rule')) cases)
    1.53 @@ -532,12 +532,12 @@
    1.54    Raw_Simplifier.rewrite_term thy Induct_Args.atomize []
    1.55    #> Object_Logic.drop_judgment thy;
    1.56  
    1.57 -val atomize_cterm = Raw_Simplifier.rewrite true Induct_Args.atomize;
    1.58 +fun atomize_cterm ctxt = Raw_Simplifier.rewrite ctxt true Induct_Args.atomize;
    1.59  
    1.60 -val atomize_tac = rewrite_goal_tac Induct_Args.atomize;
    1.61 +fun atomize_tac ctxt = rewrite_goal_tac ctxt Induct_Args.atomize;
    1.62  
    1.63 -val inner_atomize_tac =
    1.64 -  rewrite_goal_tac (map Thm.symmetric conjunction_congs) THEN' atomize_tac;
    1.65 +fun inner_atomize_tac ctxt =
    1.66 +  rewrite_goal_tac ctxt (map Thm.symmetric conjunction_congs) THEN' atomize_tac ctxt;
    1.67  
    1.68  
    1.69  (* rulify *)
    1.70 @@ -553,11 +553,11 @@
    1.71      val (As, B) = Logic.strip_horn (Thm.prop_of thm);
    1.72    in (thy, Logic.list_implies (map rulify As, rulify B)) end;
    1.73  
    1.74 -val rulify_tac =
    1.75 -  rewrite_goal_tac (Induct_Args.rulify @ conjunction_congs) THEN'
    1.76 -  rewrite_goal_tac Induct_Args.rulify_fallback THEN'
    1.77 +fun rulify_tac ctxt =
    1.78 +  rewrite_goal_tac ctxt (Induct_Args.rulify @ conjunction_congs) THEN'
    1.79 +  rewrite_goal_tac ctxt Induct_Args.rulify_fallback THEN'
    1.80    Goal.conjunction_tac THEN_ALL_NEW
    1.81 -  (rewrite_goal_tac [@{thm Pure.conjunction_imp}] THEN' Goal.norm_hhf_tac);
    1.82 +  (rewrite_goal_tac ctxt [@{thm Pure.conjunction_imp}] THEN' Goal.norm_hhf_tac ctxt);
    1.83  
    1.84  
    1.85  (* prepare rule *)
    1.86 @@ -565,9 +565,9 @@
    1.87  fun rule_instance ctxt inst rule =
    1.88    Drule.cterm_instantiate (prep_inst ctxt align_left I (Thm.prop_of rule, inst)) rule;
    1.89  
    1.90 -fun internalize k th =
    1.91 +fun internalize ctxt k th =
    1.92    th |> Thm.permute_prems 0 k
    1.93 -  |> Conv.fconv_rule (Conv.concl_conv (Thm.nprems_of th - k) atomize_cterm);
    1.94 +  |> Conv.fconv_rule (Conv.concl_conv (Thm.nprems_of th - k) (atomize_cterm ctxt));
    1.95  
    1.96  
    1.97  (* guess rule instantiation -- cannot handle pending goal parameters *)
    1.98 @@ -683,8 +683,10 @@
    1.99      | NONE => all_tac)
   1.100    end);
   1.101  
   1.102 -fun miniscope_tac p = CONVERSION o
   1.103 -  Conv.params_conv p (K (Raw_Simplifier.rewrite true [Thm.symmetric Drule.norm_hhf_eq]));
   1.104 +fun miniscope_tac p =
   1.105 +  CONVERSION o
   1.106 +    Conv.params_conv p (fn ctxt =>
   1.107 +      Raw_Simplifier.rewrite ctxt true [Thm.symmetric Drule.norm_hhf_eq]);
   1.108  
   1.109  in
   1.110  
   1.111 @@ -743,7 +745,7 @@
   1.112      val thy = Proof_Context.theory_of ctxt;
   1.113  
   1.114      val ((insts, defs), defs_ctxt) = fold_map add_defs def_insts ctxt |>> split_list;
   1.115 -    val atomized_defs = map (map (Conv.fconv_rule atomize_cterm)) defs;
   1.116 +    val atomized_defs = map (map (Conv.fconv_rule (atomize_cterm defs_ctxt))) defs;
   1.117  
   1.118      fun inst_rule (concls, r) =
   1.119        (if null insts then `Rule_Cases.get r
   1.120 @@ -774,7 +776,7 @@
   1.121    in
   1.122      (fn i => fn st =>
   1.123        ruleq
   1.124 -      |> Seq.maps (Rule_Cases.consume (flat defs) facts)
   1.125 +      |> Seq.maps (Rule_Cases.consume defs_ctxt (flat defs) facts)
   1.126        |> Seq.maps (fn (((cases, concls), (more_consumes, more_facts)), rule) =>
   1.127          (PRECISE_CONJUNCTS (length concls) (ALLGOALS (fn j =>
   1.128            (CONJUNCTS (ALLGOALS
   1.129 @@ -791,9 +793,9 @@
   1.130                   else
   1.131                     arbitrary_tac defs_ctxt k xs)
   1.132               end)
   1.133 -          THEN' inner_atomize_tac) j))
   1.134 -        THEN' atomize_tac) i st |> Seq.maps (fn st' =>
   1.135 -            guess_instance ctxt (internalize more_consumes rule) i st'
   1.136 +          THEN' inner_atomize_tac defs_ctxt) j))
   1.137 +        THEN' atomize_tac defs_ctxt) i st |> Seq.maps (fn st' =>
   1.138 +            guess_instance ctxt (internalize ctxt more_consumes rule) i st'
   1.139              |> Seq.map (rule_instance ctxt (burrow_options (Variable.polymorphic ctxt) taking))
   1.140              |> Seq.maps (fn rule' =>
   1.141                CASES (rule_cases ctxt rule' cases)
   1.142 @@ -802,7 +804,7 @@
   1.143      THEN_ALL_NEW_CASES
   1.144        ((if simp then simplify_tac ctxt THEN' (TRY o trivial_tac)
   1.145          else K all_tac)
   1.146 -       THEN_ALL_NEW rulify_tac)
   1.147 +       THEN_ALL_NEW rulify_tac ctxt)
   1.148    end;
   1.149  
   1.150  val induct_tac = gen_induct_tac (K I);
   1.151 @@ -849,7 +851,7 @@
   1.152    in
   1.153      SUBGOAL_CASES (fn (goal, i) => fn st =>
   1.154        ruleq goal
   1.155 -      |> Seq.maps (Rule_Cases.consume [] facts)
   1.156 +      |> Seq.maps (Rule_Cases.consume ctxt [] facts)
   1.157        |> Seq.maps (fn ((cases, (_, more_facts)), rule) =>
   1.158          guess_instance ctxt rule i st
   1.159          |> Seq.map (rule_instance ctxt (burrow_options (Variable.polymorphic ctxt) taking))