--- a/src/Pure/Isar/generic_target.ML Sat Apr 16 15:25:25 2011 +0200
+++ b/src/Pure/Isar/generic_target.ML Sat Apr 16 15:47:52 2011 +0200
@@ -50,8 +50,8 @@
fun define foundation ((b, mx), ((proto_b_def, atts), rhs)) lthy =
let
- val thy = ProofContext.theory_of lthy;
- val thy_ctxt = ProofContext.init_global thy;
+ val thy = Proof_Context.theory_of lthy;
+ val thy_ctxt = Proof_Context.init_global thy;
val b_def = Thm.def_binding_optional b proto_b_def;
@@ -99,8 +99,8 @@
fun import_export_proof ctxt (name, raw_th) =
let
- val thy = ProofContext.theory_of ctxt;
- val thy_ctxt = ProofContext.init_global thy;
+ val thy = Proof_Context.theory_of ctxt;
+ val thy_ctxt = Proof_Context.init_global thy;
val certT = Thm.ctyp_of thy;
val cert = Thm.cterm_of thy;
@@ -145,7 +145,7 @@
fun notes target_notes kind facts lthy =
let
- val thy = ProofContext.theory_of lthy;
+ val thy = Proof_Context.theory_of lthy;
val facts' = facts
|> map (fn (a, bs) => (a, Global_Theory.burrow_fact (Global_Theory.name_multi
(Local_Theory.full_name lthy (fst a))) bs))
@@ -155,7 +155,7 @@
in
lthy
|> target_notes kind global_facts local_facts
- |> ProofContext.note_thmss kind (Attrib.map_facts (Attrib.attribute_i thy) local_facts)
+ |> Proof_Context.note_thmss kind (Attrib.map_facts (Attrib.attribute_i thy) local_facts)
end;
@@ -163,7 +163,7 @@
fun abbrev target_abbrev prmode ((b, mx), t) lthy =
let
- val thy_ctxt = ProofContext.init_global (ProofContext.theory_of lthy);
+ val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of lthy);
val target_ctxt = Local_Theory.target_of lthy;
val t' = Assumption.export_term lthy target_ctxt t;
@@ -179,7 +179,7 @@
in
lthy
|> target_abbrev prmode (b, mx') (global_rhs, t') xs
- |> ProofContext.add_abbrev Print_Mode.internal (b, t) |> snd
+ |> Proof_Context.add_abbrev Print_Mode.internal (b, t) |> snd
|> Local_Defs.fixed_abbrev ((b, NoSyn), t)
end;
@@ -207,12 +207,12 @@
fun theory_notes kind global_facts lthy =
let
- val thy = ProofContext.theory_of lthy;
+ val thy = Proof_Context.theory_of lthy;
val global_facts' = Attrib.map_facts (Attrib.attribute_i thy) global_facts;
in
lthy
|> Local_Theory.background_theory (Global_Theory.note_thmss kind global_facts' #> snd)
- |> Local_Theory.target (ProofContext.note_thmss kind global_facts' #> snd)
+ |> Local_Theory.target (Proof_Context.note_thmss kind global_facts' #> snd)
end;
fun theory_abbrev prmode ((b, mx), t) =