ProofContext.init;
authorwenzelm
Fri Nov 24 22:05:12 2006 +0100 (2006-11-24)
changeset 21516c2a116a2c4fd
parent 21515 43d55165b282
child 21517 b165c9120702
ProofContext.init;
src/HOL/Nominal/nominal_package.ML
src/HOL/Tools/datatype_codegen.ML
src/Provers/classical.ML
src/Pure/goal.ML
src/Pure/meta_simplifier.ML
     1.1 --- a/src/HOL/Nominal/nominal_package.ML	Fri Nov 24 17:23:15 2006 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_package.ML	Fri Nov 24 22:05:12 2006 +0100
     1.3 @@ -1549,7 +1549,7 @@
     1.4              val y = Free ("y", U);
     1.5              val y' = Free ("y'", U)
     1.6            in
     1.7 -            standard (Goal.prove (Context.init_proof thy11) [] (finite_prems @
     1.8 +            standard (Goal.prove (ProofContext.init thy11) [] (finite_prems @
     1.9                  [HOLogic.mk_Trueprop (R $ x $ y),
    1.10                   HOLogic.mk_Trueprop (HOLogic.mk_all ("y'", U,
    1.11                     HOLogic.mk_imp (R $ x $ y', HOLogic.mk_eq (y', y)))),
    1.12 @@ -1652,7 +1652,7 @@
    1.13           Const ("Finite_Set.Finites", HOLogic.mk_setT (HOLogic.mk_setT aT))))) dt_atomTs;
    1.14  
    1.15      val rec_unique_thms = split_conj_thm (Goal.prove
    1.16 -      (Context.init_proof thy11) (map fst rec_unique_frees)
    1.17 +      (ProofContext.init thy11) (map fst rec_unique_frees)
    1.18        (List.concat finite_premss @ finite_ctxt_prems @ rec_prems @ rec_prems')
    1.19        (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj rec_unique_concls))
    1.20        (fn {prems, context} =>
     2.1 --- a/src/HOL/Tools/datatype_codegen.ML	Fri Nov 24 17:23:15 2006 +0100
     2.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Fri Nov 24 22:05:12 2006 +0100
     2.3 @@ -380,13 +380,15 @@
     2.4    val rew_conj = thm "HOL.atomize_conj" |> Thm.symmetric;
     2.5    val not_false_true = iffD2 OF [nth (thms "HOL.simp_thms") 7, TrueI];
     2.6    val not_eq_quodlibet = thm "not_eq_quodlibet";
     2.7 -in fun get_cert_datatype thy dtco =
     2.8 +in
     2.9 +
    2.10 +fun get_cert_datatype thy dtco =
    2.11    let
    2.12      val SOME (vs, cs) = DatatypePackage.get_datatype_spec thy dtco;
    2.13      val inject = (#inject o DatatypePackage.the_datatype thy) dtco
    2.14        |> map (fn thm => bool_eq_implies OF [thm] )
    2.15        |> map (Tactic.rewrite_rule [rew_eq, rew_conj]);
    2.16 -    val ctxt = Context.init_proof thy;
    2.17 +    val ctxt = ProofContext.init thy;
    2.18      val simpset = Simplifier.context ctxt
    2.19        (MetaSimplifier.empty_ss addsimprocs [DatatypePackage.distinct_simproc]);
    2.20      val cos = map (fn (co, tys) =>
    2.21 @@ -398,12 +400,15 @@
    2.22        |> map (fn t => Goal.prove_global thy [] [] t (K tac))
    2.23        |> map (fn thm => not_eq_quodlibet OF [thm])
    2.24    in inject @ distinct end
    2.25 -end (*local*);
    2.26 +
    2.27 +end;
    2.28  
    2.29  local
    2.30    val not_sym = thm "HOL.not_sym";
    2.31    val not_false_true = iffD2 OF [nth (thms "HOL.simp_thms") 7, TrueI];
    2.32 -in fun get_eq_datatype thy dtco =
    2.33 +in
    2.34 +
    2.35 +fun get_eq_datatype thy dtco =
    2.36    let
    2.37      val SOME (vs, cs) = DatatypePackage.get_datatype_spec thy dtco;
    2.38      fun mk_triv_inject co =
    2.39 @@ -418,7 +423,7 @@
    2.40        in eqTrueI OF [Thm.instantiate ([(cty, cty')], [(ct, ct')]) HOL.refl] end;
    2.41      val inject1 = map_filter (fn (co, []) => SOME (mk_triv_inject co) | _ => NONE) cs
    2.42      val inject2 = (#inject o DatatypePackage.the_datatype thy) dtco;
    2.43 -    val ctxt = Context.init_proof thy;
    2.44 +    val ctxt = ProofContext.init thy;
    2.45      val simpset = Simplifier.context ctxt
    2.46        (MetaSimplifier.empty_ss addsimprocs [distinct_simproc]);
    2.47      val cos = map (fn (co, tys) =>
    2.48 @@ -430,7 +435,8 @@
    2.49        |> map (fn t => Goal.prove_global thy [] [] t (K tac))
    2.50        |> (fn thms => thms @ map (fn thm => not_sym OF [thm]) thms)
    2.51    in inject1 @ inject2 @ distinct end;
    2.52 -end (*local*);
    2.53 +
    2.54 +end;
    2.55  
    2.56  fun add_datatype_case_const dtco thy =
    2.57    let
     3.1 --- a/src/Provers/classical.ML	Fri Nov 24 17:23:15 2006 +0100
     3.2 +++ b/src/Provers/classical.ML	Fri Nov 24 22:05:12 2006 +0100
     3.3 @@ -888,7 +888,7 @@
     3.4  
     3.5  fun claset_of thy =
     3.6    let val (cs_ref, ctxt_cs) = GlobalClaset.get thy
     3.7 -  in context_cs (Context.init_proof thy) (! cs_ref) (ctxt_cs) end;
     3.8 +  in context_cs (ProofContext.init thy) (! cs_ref) (ctxt_cs) end;
     3.9  val claset = claset_of o Context.the_context;
    3.10  
    3.11  fun CLASET tacf st = tacf (claset_of (Thm.theory_of_thm st)) st;
     4.1 --- a/src/Pure/goal.ML	Fri Nov 24 17:23:15 2006 +0100
     4.2 +++ b/src/Pure/goal.ML	Fri Nov 24 22:05:12 2006 +0100
     4.3 @@ -106,7 +106,7 @@
     4.4  
     4.5  fun prove_multi ctxt xs asms props tac =
     4.6    let
     4.7 -    val thy = Context.theory_of_proof ctxt;
     4.8 +    val thy = ProofContext.theory_of ctxt;
     4.9      val string_of_term = Sign.string_of_term thy;
    4.10  
    4.11      fun err msg = cat_error msg
    4.12 @@ -145,7 +145,7 @@
    4.13  fun prove ctxt xs asms prop tac = hd (prove_multi ctxt xs asms [prop] tac);
    4.14  
    4.15  fun prove_global thy xs asms prop tac =
    4.16 -  Drule.standard (prove (Context.init_proof thy) xs asms prop (fn {prems, ...} => tac prems));
    4.17 +  Drule.standard (prove (ProofContext.init thy) xs asms prop (fn {prems, ...} => tac prems));
    4.18  
    4.19  
    4.20  
     5.1 --- a/src/Pure/meta_simplifier.ML	Fri Nov 24 17:23:15 2006 +0100
     5.2 +++ b/src/Pure/meta_simplifier.ML	Fri Nov 24 22:05:12 2006 +0100
     5.3 @@ -366,7 +366,7 @@
     5.4  fun context ctxt =
     5.5    map_simpset1 (fn (rules, prems, bounds, _) => (rules, prems, bounds, SOME ctxt));
     5.6  
     5.7 -val theory_context = context o Context.init_proof;
     5.8 +val theory_context = context o ProofContext.init;
     5.9  
    5.10  fun fallback_context _ (ss as Simpset ({context = SOME _, ...}, _)) = ss
    5.11    | fallback_context thy ss =