src/Tools/induct.ML
changeset 42361 23f352990944
parent 42284 326f57825e1a
child 42488 4638622bcaa1
     1.1 --- a/src/Tools/induct.ML	Sat Apr 16 15:47:52 2011 +0200
     1.2 +++ b/src/Tools/induct.ML	Sat Apr 16 16:15:37 2011 +0200
     1.3 @@ -128,7 +128,7 @@
     1.4        Conv.implies_concl_conv (swap_prems_conv (i - 1)) then_conv
     1.5        Conv.rewr_conv Drule.swap_prems_eq
     1.6  
     1.7 -fun drop_judgment ctxt = Object_Logic.drop_judgment (ProofContext.theory_of ctxt);
     1.8 +fun drop_judgment ctxt = Object_Logic.drop_judgment (Proof_Context.theory_of ctxt);
     1.9  
    1.10  fun find_eq ctxt t =
    1.11    let
    1.12 @@ -386,7 +386,7 @@
    1.13  
    1.14  fun prep_inst ctxt align tune (tm, ts) =
    1.15    let
    1.16 -    val cert = Thm.cterm_of (ProofContext.theory_of ctxt);
    1.17 +    val cert = Thm.cterm_of (Proof_Context.theory_of ctxt);
    1.18      fun prep_var (x, SOME t) =
    1.19            let
    1.20              val cx = cert x;
    1.21 @@ -470,7 +470,7 @@
    1.22  
    1.23  fun cases_tac ctxt simp insts opt_rule facts =
    1.24    let
    1.25 -    val thy = ProofContext.theory_of ctxt;
    1.26 +    val thy = Proof_Context.theory_of ctxt;
    1.27  
    1.28      fun inst_rule r =
    1.29        (if null insts then r
    1.30 @@ -573,7 +573,7 @@
    1.31  
    1.32  fun guess_instance ctxt rule i st =
    1.33    let
    1.34 -    val thy = ProofContext.theory_of ctxt;
    1.35 +    val thy = Proof_Context.theory_of ctxt;
    1.36      val maxidx = Thm.maxidx_of st;
    1.37      val goal = Thm.term_of (Thm.cprem_of st i);  (*exception Subscript*)
    1.38      val params = rev (Term.rename_wrt_term goal (Logic.strip_params goal));
    1.39 @@ -599,7 +599,7 @@
    1.40  
    1.41  fun special_rename_params ctxt [[SOME (Free (z, Type (T, _)))]] [thm] =
    1.42        let
    1.43 -        val x = Name.clean (ProofContext.revert_skolem ctxt z);
    1.44 +        val x = Name.clean (Proof_Context.revert_skolem ctxt z);
    1.45          fun index i [] = []
    1.46            | index i (y :: ys) =
    1.47                if x = y then x ^ string_of_int i :: index (i + 1) ys
    1.48 @@ -640,13 +640,13 @@
    1.49  
    1.50  fun meta_spec_tac ctxt n (x, T) = SUBGOAL (fn (goal, i) =>
    1.51    let
    1.52 -    val thy = ProofContext.theory_of ctxt;
    1.53 +    val thy = Proof_Context.theory_of ctxt;
    1.54      val cert = Thm.cterm_of thy;
    1.55  
    1.56      val v = Free (x, T);
    1.57      fun spec_rule prfx (xs, body) =
    1.58        @{thm Pure.meta_spec}
    1.59 -      |> Thm.rename_params_rule ([Name.clean (ProofContext.revert_skolem ctxt x)], 1)
    1.60 +      |> Thm.rename_params_rule ([Name.clean (Proof_Context.revert_skolem ctxt x)], 1)
    1.61        |> Thm.lift_rule (cert prfx)
    1.62        |> `(Thm.prop_of #> Logic.strip_assums_concl)
    1.63        |-> (fn pred $ arg =>
    1.64 @@ -722,7 +722,7 @@
    1.65  
    1.66  fun induct_tac ctxt simp def_insts arbitrary taking opt_rule facts =
    1.67    let
    1.68 -    val thy = ProofContext.theory_of ctxt;
    1.69 +    val thy = Proof_Context.theory_of ctxt;
    1.70  
    1.71      val ((insts, defs), defs_ctxt) = fold_map add_defs def_insts ctxt |>> split_list;
    1.72      val atomized_defs = map (map (Conv.fconv_rule atomize_cterm)) defs;
    1.73 @@ -777,7 +777,7 @@
    1.74              |> Seq.maps (fn rule' =>
    1.75                CASES (rule_cases ctxt rule' cases)
    1.76                  (Tactic.rtac rule' i THEN
    1.77 -                  PRIMITIVE (singleton (ProofContext.export defs_ctxt ctxt))) st'))))
    1.78 +                  PRIMITIVE (singleton (Proof_Context.export defs_ctxt ctxt))) st'))))
    1.79      THEN_ALL_NEW_CASES
    1.80        ((if simp then simplify_tac ctxt THEN' (TRY o trivial_tac)
    1.81          else K all_tac)
    1.82 @@ -809,7 +809,7 @@
    1.83  
    1.84  fun coinduct_tac ctxt inst taking opt_rule facts =
    1.85    let
    1.86 -    val thy = ProofContext.theory_of ctxt;
    1.87 +    val thy = Proof_Context.theory_of ctxt;
    1.88  
    1.89      fun inst_rule r =
    1.90        if null inst then `Rule_Cases.get r