--- a/src/Pure/ML/ml_thms.ML Mon May 31 19:36:13 2010 +0200
+++ b/src/Pure/ML/ml_thms.ML Mon May 31 21:06:57 2010 +0200
@@ -15,15 +15,15 @@
(* auxiliary facts table *)
-structure AuxFacts = Proof_Data
+structure Aux_Facts = Proof_Data
(
type T = thm list Inttab.table;
fun init _ = Inttab.empty;
);
-val put_thms = AuxFacts.map o Inttab.update;
+val put_thms = Aux_Facts.map o Inttab.update;
-fun the_thms ctxt name = the (Inttab.lookup (AuxFacts.get ctxt) name);
+fun the_thms ctxt name = the (Inttab.lookup (Aux_Facts.get ctxt) name);
fun the_thm ctxt name = the_single (the_thms ctxt name);
fun thm_bind kind a i =