equal
deleted
inserted
replaced
13 structure ML_Thms: ML_THMS = |
13 structure ML_Thms: ML_THMS = |
14 struct |
14 struct |
15 |
15 |
16 (* auxiliary facts table *) |
16 (* auxiliary facts table *) |
17 |
17 |
18 structure AuxFacts = Proof_Data |
18 structure Aux_Facts = Proof_Data |
19 ( |
19 ( |
20 type T = thm list Inttab.table; |
20 type T = thm list Inttab.table; |
21 fun init _ = Inttab.empty; |
21 fun init _ = Inttab.empty; |
22 ); |
22 ); |
23 |
23 |
24 val put_thms = AuxFacts.map o Inttab.update; |
24 val put_thms = Aux_Facts.map o Inttab.update; |
25 |
25 |
26 fun the_thms ctxt name = the (Inttab.lookup (AuxFacts.get ctxt) name); |
26 fun the_thms ctxt name = the (Inttab.lookup (Aux_Facts.get ctxt) name); |
27 fun the_thm ctxt name = the_single (the_thms ctxt name); |
27 fun the_thm ctxt name = the_single (the_thms ctxt name); |
28 |
28 |
29 fun thm_bind kind a i = |
29 fun thm_bind kind a i = |
30 "val " ^ a ^ " = ML_Thms.the_" ^ kind ^ |
30 "val " ^ a ^ " = ML_Thms.the_" ^ kind ^ |
31 " (ML_Context.the_local_context ()) " ^ string_of_int i ^ ";\n"; |
31 " (ML_Context.the_local_context ()) " ^ string_of_int i ^ ";\n"; |