1.1 --- a/src/Pure/ML/ml_thms.ML Mon May 31 19:36:13 2010 +0200
1.2 +++ b/src/Pure/ML/ml_thms.ML Mon May 31 21:06:57 2010 +0200
1.3 @@ -15,15 +15,15 @@
1.4
1.5 (* auxiliary facts table *)
1.6
1.7 -structure AuxFacts = Proof_Data
1.8 +structure Aux_Facts = Proof_Data
1.9 (
1.10 type T = thm list Inttab.table;
1.11 fun init _ = Inttab.empty;
1.12 );
1.13
1.14 -val put_thms = AuxFacts.map o Inttab.update;
1.15 +val put_thms = Aux_Facts.map o Inttab.update;
1.16
1.17 -fun the_thms ctxt name = the (Inttab.lookup (AuxFacts.get ctxt) name);
1.18 +fun the_thms ctxt name = the (Inttab.lookup (Aux_Facts.get ctxt) name);
1.19 fun the_thm ctxt name = the_single (the_thms ctxt name);
1.20
1.21 fun thm_bind kind a i =