# HG changeset patch
# User wenzelm
# Date 1205968849 -3600
# Node ID f70620a4cf8110bc1155cd806c11680912d3783d
# Parent  04dacc6809b622d789d6262cab81b3b4f30da7ab
renamed former get_thms(_silent) to get_fact(_silent);

diff -r 04dacc6809b6 -r f70620a4cf81 src/Pure/Isar/attrib.ML
--- 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
diff -r 04dacc6809b6 -r f70620a4cf81 src/Pure/Isar/locale.ML
--- 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;
diff -r 04dacc6809b6 -r f70620a4cf81 src/Pure/Isar/specification.ML
--- 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 *)