src/Pure/ML/ml_thms.ML
changeset 37216 3165bc303f66
parent 36950 75b8f26f2f07
child 41625 08240feb69c7
     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 =