--- a/src/Pure/Isar/attrib.ML Thu Mar 20 00:20:48 2008 +0100
+++ b/src/Pure/Isar/attrib.ML Thu Mar 20 00:20:49 2008 +0100
@@ -162,7 +162,7 @@
fun gen_thm pick = Scan.depend (fn context =>
let
val thy = Context.theory_of context;
- val get = Context.cases PureThy.get_thms ProofContext.get_thms context;
+ val get = Context.cases PureThy.get_fact ProofContext.get_fact context;
fun get_fact s = get (Facts.Fact s);
fun get_named s = get (Facts.Named (s, NONE));
in
--- a/src/Pure/Isar/locale.ML Thu Mar 20 00:20:48 2008 +0100
+++ b/src/Pure/Isar/locale.ML Thu Mar 20 00:20:49 2008 +0100
@@ -1407,7 +1407,7 @@
in
-fun read_facts x = prep_facts check_name ProofContext.get_thms Attrib.intern_src x;
+fun read_facts x = prep_facts check_name ProofContext.get_fact Attrib.intern_src x;
fun cert_facts x = prep_facts I (K I) (K I) x;
end;
--- a/src/Pure/Isar/specification.ML Thu Mar 20 00:20:48 2008 +0100
+++ b/src/Pure/Isar/specification.ML Thu Mar 20 00:20:49 2008 +0100
@@ -213,18 +213,18 @@
(* fact statements *)
-fun gen_theorems prep_thms prep_att kind raw_facts lthy =
+fun gen_theorems prep_fact prep_att kind raw_facts lthy =
let
val attrib = prep_att (ProofContext.theory_of lthy);
val facts = raw_facts |> map (fn ((name, atts), bs) =>
((name, map attrib atts),
- bs |> map (fn (b, more_atts) => (prep_thms lthy b, map attrib more_atts))));
+ bs |> map (fn (b, more_atts) => (prep_fact lthy b, map attrib more_atts))));
val (res, lthy') = lthy |> LocalTheory.notes kind facts;
val _ = ProofDisplay.present_results lthy' ((kind, ""), res);
in (res, lthy') end;
val theorems = gen_theorems (K I) (K I);
-val theorems_cmd = gen_theorems ProofContext.get_thms Attrib.intern_src;
+val theorems_cmd = gen_theorems ProofContext.get_fact Attrib.intern_src;
(* complex goal statements *)