# HG changeset patch
# User huffman
# Date 1321345339 -3600
# Node ID 697e387bb859c18a00af37b901f8e6fdfbe59301
# Parent  e2e27909bb66128063eeb5aa40af33cc0aa49f94# Parent  4a23d6cb6cdadece25f3e45769c74721fc25316b
merged

diff -r e2e27909bb66 -r 697e387bb859 src/HOL/Library/Code_Real_Approx_By_Float.thy
--- a/src/HOL/Library/Code_Real_Approx_By_Float.thy	Mon Nov 14 19:35:41 2011 +0100
+++ b/src/HOL/Library/Code_Real_Approx_By_Float.thy	Tue Nov 15 09:22:19 2011 +0100
@@ -140,7 +140,4 @@
   ultimately show "False" by blast
 qed
 
-lemma False
-  sorry -- "Use quick_and_dirty to load this theory."
-
 end
diff -r e2e27909bb66 -r 697e387bb859 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Mon Nov 14 19:35:41 2011 +0100
+++ b/src/Pure/Isar/attrib.ML	Tue Nov 15 09:22:19 2011 +0100
@@ -25,7 +25,6 @@
     (('c * 'a list) * ('b * 'a list) list) list ->
     (('c * 'att list) * ('fact * 'att list) list) list
   val eval_thms: Proof.context -> (Facts.ref * src list) list -> thm list
-  val crude_closure: Proof.context -> src -> src
   val setup: Binding.binding -> attribute context_parser -> string -> theory -> theory
   val attribute_setup: bstring * Position.T -> Symbol_Pos.text * Position.T -> string ->
     theory -> theory
@@ -34,8 +33,11 @@
   val thm: thm context_parser
   val thms: thm list context_parser
   val multi_thm: thm list context_parser
+  val partial_evaluation: Proof.context ->
+    (binding * (thm list * Args.src list) list) list ->
+    (binding * (thm list * Args.src list) list) list
+  val internal: (morphism -> attribute) -> src
   val print_configs: Proof.context -> unit
-  val internal: (morphism -> attribute) -> src
   val config_bool: Binding.binding ->
     (Context.generic -> bool) -> bool Config.T * (theory -> theory)
   val config_int: Binding.binding ->
@@ -142,19 +144,6 @@
   |> fst |> maps snd;
 
 
-(* crude_closure *)
-
-(*Produce closure without knowing facts in advance! The following
-  works reasonably well for attribute parsers that do not peek at the
-  thm structure.*)
-
-fun crude_closure ctxt src =
- (try (fn () =>
-    Thm.apply_attribute (attribute_i (Proof_Context.theory_of ctxt) src)
-      (Context.Proof ctxt, Drule.asm_rl)) ();
-  Args.closure src);
-
-
 (* attribute setup *)
 
 fun syntax scan = Args.syntax "attribute" scan;
@@ -227,6 +216,48 @@
 
 
 
+(** partial evaluation **)
+
+local
+(* FIXME assignable, closure (!?) *)
+
+fun apply_att src (context, th) =
+  attribute_i (Context.theory_of context) src (context, th);
+
+fun eval src (th, (decls, context)) =
+  (case apply_att src (context, th) of
+    (NONE, SOME th') => (th', (decls, context))
+  | (opt_context', opt_th') =>
+      let
+        val context' = the_default context opt_context';
+        val th' = the_default th opt_th';
+        val decls' =
+          (case decls of
+            [] => [(th, [src])]
+          | (th2, srcs2) :: rest =>
+              if op = (pairself Thm.rep_thm (th, th2))  (* FIXME derivation!? *)
+              then ((th2, src :: srcs2) :: rest)
+              else (th, [src]) :: (th2, srcs2) :: rest);
+      in (th', (decls', context')) end);
+
+in
+
+fun partial_evaluation ctxt facts =
+  let
+    val (facts', (decls, _)) =
+      (facts, ([], Context.Proof ctxt)) |-> fold_map (fn ((b, more_atts), fact) => fn res =>
+        let
+          val (thss', res') =
+            (fact, res) |-> fold_map (fn (ths, atts) =>
+              fold_map (curry (fold eval (atts @ more_atts))) ths);
+        in (((b, []), [(flat thss', [])]), res') end);
+    val decl_fact = (empty_binding, rev (map (fn (th, atts) => ([th], rev atts)) decls));
+  in decl_fact :: facts' end;
+
+end;
+
+
+
 (** basic attributes **)
 
 (* internal *)
diff -r e2e27909bb66 -r 697e387bb859 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Mon Nov 14 19:35:41 2011 +0100
+++ b/src/Pure/Isar/locale.ML	Tue Nov 15 09:22:19 2011 +0100
@@ -555,19 +555,19 @@
 
 (* Theorems *)
 
-fun add_thmss loc kind args ctxt =
+fun add_thmss loc kind facts ctxt =
   let
-    val (Notes args', ctxt') = Element.activate_i (Notes (kind, args)) ctxt;
+    val (Notes facts', ctxt') = Element.activate_i (Notes (kind, facts)) ctxt;
     val ctxt'' = ctxt' |> Proof_Context.background_theory
-     ((change_locale loc o apfst o apsnd) (cons (args', serial ()))
+     ((change_locale loc o apfst o apsnd) (cons (facts', serial ()))
         #>
       (* Registrations *)
       (fn thy => fold_rev (fn (_, morph) =>
             let
-              val args'' = snd args'
+              val facts'' = snd facts'
                 |> Element.facts_map (Element.transform_ctxt morph)
                 |> Attrib.map_facts (map (Attrib.attribute_i thy));
-            in Global_Theory.note_thmss kind args'' #> snd end)
+            in Global_Theory.note_thmss kind facts'' #> snd end)
         (registrations_of (Context.Theory thy) loc) thy))
   in ctxt'' end;