# HG changeset patch
# User wenzelm
# Date 1160353207 -7200
# Node ID 3f065aa897925d4a0156b654e4493af8424bd5f8
# Parent  7a4dceafab2d64cc3fa39f375d3218f75df8aca8
added theorems(_i) -- with present_results;

diff -r 7a4dceafab2d -r 3f065aa89792 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Mon Oct 09 02:20:06 2006 +0200
+++ b/src/Pure/Isar/specification.ML	Mon Oct 09 02:20:07 2006 +0200
@@ -36,6 +36,10 @@
     local_theory -> local_theory
   val const_syntax: Syntax.mode -> (xstring * mixfix) list -> local_theory -> local_theory
   val const_syntax_i: Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory
+  val theorems: string -> ((bstring * Attrib.src list) * (thmref * Attrib.src list) list) list
+    -> local_theory -> (bstring * thm list) list * local_theory
+  val theorems_i: string -> ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list
+    -> local_theory -> (bstring * thm list) list * local_theory
 end;
 
 structure Specification: SPECIFICATION =
@@ -49,6 +53,9 @@
   | print_consts ctxt pred cs =
       if ! quiet_mode then () else Pretty.writeln (ProofDisplay.pretty_consts ctxt pred cs);
 
+fun present_results ctxt kind res =
+  if ! quiet_mode then () else ProofDisplay.present_results ctxt ((kind, ""), res);
+
 
 (* prepare specification *)
 
@@ -84,6 +91,7 @@
 
     val ((consts, axioms), lthy') = lthy
       |> LocalTheory.consts spec_frees vars
+      ||> fold (fold Variable.fix_frees o snd) specs   (* FIXME !? *)
       ||>> LocalTheory.axioms specs;
 
     (* FIXME generic target!? *)
@@ -114,7 +122,7 @@
 (*          |> LocalTheory.def ((x, mx), ((name ^ "_raw", []), rhs));  FIXME *)
           |> LocalTheory.def ((x, mx), ((name, []), rhs));
         val ((b, [th']), lthy3) = lthy2
-          |> LocalTheory.note ((name, atts), [prove lthy2 lhs th]);
+          |> LocalTheory.note ((name, atts), [prove lthy2 th]);
       in (((x, T), (lhs, (b, th'))), LocalTheory.reinit lthy3) end;
 
     val ((cs, defs), lthy') = lthy |> fold_map define args |>> split_list;
@@ -165,4 +173,21 @@
 val const_syntax = gen_syntax Consts.intern;
 val const_syntax_i = gen_syntax (K I);
 
+
+(* theorems *)
+
+fun gen_theorems prep_thms prep_att kind raw_facts lthy =
+  let
+    val k = if kind = "" then [] else [Attrib.kind kind];
+    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 @ k))));
+    val (res, lthy') = lthy |> LocalTheory.notes facts;
+    val _ = present_results lthy' kind res;
+  in (res, lthy') end;
+
+val theorems = gen_theorems ProofContext.get_thms Attrib.intern_src;
+val theorems_i = gen_theorems (K I) (K I);
+
 end;