1.1 --- a/src/Tools/induct.ML	Fri Aug 28 18:23:24 2009 +0200
     1.2 +++ b/src/Tools/induct.ML	Fri Aug 28 21:04:03 2009 +0200
     1.3 @@ -288,21 +288,21 @@
     1.4  
     1.5  (* prep_inst *)
     1.6  
     1.7 -fun prep_inst thy align tune (tm, ts) =
     1.8 +fun prep_inst ctxt align tune (tm, ts) =
     1.9    let
    1.10 -    val cert = Thm.cterm_of thy;
    1.11 +    val cert = Thm.cterm_of (ProofContext.theory_of ctxt);
    1.12      fun prep_var (x, SOME t) =
    1.13            let
    1.14              val cx = cert x;
    1.15              val xT = #T (Thm.rep_cterm cx);
    1.16              val ct = cert (tune t);
    1.17 -            val tT = Thm.ctyp_of_term ct;
    1.18 +            val tT = #T (Thm.rep_cterm ct);
    1.19            in
    1.20 -            if Type.could_unify (Thm.typ_of tT, xT) then SOME (cx, ct)
    1.21 +            if Type.could_unify (tT, xT) then SOME (cx, ct)
    1.22              else error (Pretty.string_of (Pretty.block
    1.23               [Pretty.str "Ill-typed instantiation:", Pretty.fbrk,
    1.24 -              Display.pretty_cterm ct, Pretty.str " ::", Pretty.brk 1,
    1.25 -              Display.pretty_ctyp (#T (Thm.crep_cterm ct))]))
    1.26 +              Syntax.pretty_term ctxt (Thm.term_of ct), Pretty.str " ::", Pretty.brk 1,
    1.27 +              Syntax.pretty_typ ctxt tT]))
    1.28            end
    1.29        | prep_var (_, NONE) = NONE;
    1.30      val xs = vars_of tm;
    1.31 @@ -342,12 +342,11 @@
    1.32  fun cases_tac ctxt insts opt_rule facts =
    1.33    let
    1.34      val thy = ProofContext.theory_of ctxt;
    1.35 -    val cert = Thm.cterm_of thy;
    1.36  
    1.37      fun inst_rule r =
    1.38        if null insts then `RuleCases.get r
    1.39        else (align_left "Rule has fewer premises than arguments given" (Thm.prems_of r) insts
    1.40 -        |> maps (prep_inst thy align_left I)
    1.41 +        |> maps (prep_inst ctxt align_left I)
    1.42          |> Drule.cterm_instantiate) r |> pair (RuleCases.get r);
    1.43  
    1.44      val ruleq =
    1.45 @@ -411,8 +410,8 @@
    1.46  
    1.47  (* prepare rule *)
    1.48  
    1.49 -fun rule_instance thy inst rule =
    1.50 -  Drule.cterm_instantiate (prep_inst thy align_left I (Thm.prop_of rule, inst)) rule;
    1.51 +fun rule_instance ctxt inst rule =
    1.52 +  Drule.cterm_instantiate (prep_inst ctxt align_left I (Thm.prop_of rule, inst)) rule;
    1.53  
    1.54  fun internalize k th =
    1.55    th |> Thm.permute_prems 0 k
    1.56 @@ -589,7 +588,7 @@
    1.57        (if null insts then `RuleCases.get r
    1.58         else (align_left "Rule has fewer conclusions than arguments given"
    1.59            (map Logic.strip_imp_concl (Logic.dest_conjunctions (Thm.concl_of r))) insts
    1.60 -        |> maps (prep_inst thy align_right (atomize_term thy))
    1.61 +        |> maps (prep_inst ctxt align_right (atomize_term thy))
    1.62          |> Drule.cterm_instantiate) r |> pair (RuleCases.get r))
    1.63        |> (fn ((cases, consumes), th) => (((cases, concls), consumes), th));
    1.64  
    1.65 @@ -619,7 +618,7 @@
    1.66            THEN' inner_atomize_tac) j))
    1.67          THEN' atomize_tac) i st |> Seq.maps (fn st' =>
    1.68              guess_instance ctxt (internalize more_consumes rule) i st'
    1.69 -            |> Seq.map (rule_instance thy (burrow_options (Variable.polymorphic ctxt) taking))
    1.70 +            |> Seq.map (rule_instance ctxt (burrow_options (Variable.polymorphic ctxt) taking))
    1.71              |> Seq.maps (fn rule' =>
    1.72                CASES (rule_cases rule' cases)
    1.73                  (Tactic.rtac rule' i THEN
    1.74 @@ -657,7 +656,7 @@
    1.75  
    1.76      fun inst_rule r =
    1.77        if null inst then `RuleCases.get r
    1.78 -      else Drule.cterm_instantiate (prep_inst thy align_right I (main_prop_of r, inst)) r
    1.79 +      else Drule.cterm_instantiate (prep_inst ctxt align_right I (main_prop_of r, inst)) r
    1.80          |> pair (RuleCases.get r);
    1.81  
    1.82      fun ruleq goal =
    1.83 @@ -673,7 +672,7 @@
    1.84        |> Seq.maps (RuleCases.consume [] facts)
    1.85        |> Seq.maps (fn ((cases, (_, more_facts)), rule) =>
    1.86          guess_instance ctxt rule i st
    1.87 -        |> Seq.map (rule_instance thy (burrow_options (Variable.polymorphic ctxt) taking))
    1.88 +        |> Seq.map (rule_instance ctxt (burrow_options (Variable.polymorphic ctxt) taking))
    1.89          |> Seq.maps (fn rule' =>
    1.90            CASES (RuleCases.make_common false (thy, Thm.prop_of rule') cases)
    1.91              (Method.insert_tac more_facts i THEN Tactic.rtac rule' i) st)))