# HG changeset patch
# User wenzelm
# Date 1126952285 -7200
# Node ID 429ca1e212893513bd666a162a52e1c597c22dfd
# Parent  b94e2897776adfb7ef296b6542110c732a437d52
interpretation: use goal commands without target -- no storing of results;

diff -r b94e2897776a -r 429ca1e21289 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Sat Sep 17 12:18:04 2005 +0200
+++ b/src/Pure/Isar/locale.ML	Sat Sep 17 12:18:05 2005 +0200
@@ -1689,13 +1689,10 @@
 
 (* note_thmss_qualified *)
 
-fun theory_qualified name =
-  Theory.add_path (Sign.base_name name)
-  #> Theory.no_base_names;
-
 fun note_thmss_qualified kind name args thy =
   thy
-  |> theory_qualified name
+  |> Theory.add_path (Sign.base_name name)
+  |> Theory.no_base_names
   |> PureThy.note_thmss_i (Drule.kind kind) args
   |>> Theory.restore_naming thy;
 
@@ -2062,19 +2059,19 @@
     val (_, (_, view), _, ctxt, propp) = prep_stmt NONE elems (map snd concl) thy_ctxt;
     val ctxt' = ctxt |> ProofContext.add_view thy_ctxt view;
     val stmt = map fst concl ~~ propp;
-  in global_goal prep_att kind after_qed NONE a stmt ctxt' end;
-
-fun gen_theorem_in_locale prep_locale prep_src prep_elem prep_stmt
+  in global_goal prep_att kind after_qed (SOME "") a stmt ctxt' end;
+
+fun gen_theorem_in_locale prep_locale prep_src prep_elem prep_stmt no_target
     kind after_qed raw_locale (name, atts) raw_elems concl thy =
   let
     val locale = prep_locale thy raw_locale;
     val locale_atts = map (prep_src thy) atts;
     val locale_attss = map (map (prep_src thy) o snd o fst) concl;
-    val target = SOME (extern thy locale);
+    val target = if no_target then NONE else SOME (extern thy locale);
     val elems = map (prep_elem thy) raw_elems;
     val names = map (fst o fst) concl;
 
-    val thy_ctxt = thy |> theory_qualified locale |> ProofContext.init;
+    val thy_ctxt = ProofContext.init thy;
     val (_, (locale_view, elems_view), locale_ctxt, elems_ctxt, propp) =
       prep_stmt (SOME raw_locale) elems (map snd concl) thy_ctxt;
     val elems_ctxt' = elems_ctxt |> ProofContext.add_view locale_ctxt elems_view;
@@ -2086,8 +2083,7 @@
     fun after_qed' (goal_ctxt, raw_results) results =
       let val res = results |> (map o map)
           (ProofContext.export_standard elems_ctxt' locale_ctxt) in
-        Sign.restore_naming thy
-        #> curry (add_thmss kind locale ((names ~~ locale_attss) ~~ res)) locale_ctxt
+        curry (add_thmss kind locale ((names ~~ locale_attss) ~~ res)) locale_ctxt
         #-> (fn res' =>
           if name = "" andalso null locale_atts then I
           else #2 o add_thmss kind locale [((name, locale_atts), List.concat (map #2 res'))])
@@ -2100,13 +2096,14 @@
 
 val theorem = gen_theorem Attrib.global_attribute intern_attrib_elem_expr read_context_statement;
 val theorem_i = gen_theorem (K I) (K I) cert_context_statement;
-val theorem_in_locale =
-  gen_theorem_in_locale intern Attrib.intern_src intern_attrib_elem_expr read_context_statement;
-val theorem_in_locale_i =
-  gen_theorem_in_locale (K I) (K I) (K I) cert_context_statement;
+val theorem_in_locale = gen_theorem_in_locale intern Attrib.intern_src
+  intern_attrib_elem_expr read_context_statement false;
+val theorem_in_locale_i = gen_theorem_in_locale (K I) (K I) (K I) cert_context_statement false;
+val theorem_in_locale_no_target =
+  gen_theorem_in_locale (K I) (K I) (K I) cert_context_statement true;
 
 fun smart_theorem kind NONE a [] concl =
-      Proof.theorem kind (K (K I)) NONE a concl o ProofContext.init
+      Proof.theorem kind (K (K I)) (SOME "") a concl o ProofContext.init
   | smart_theorem kind NONE a elems concl =
       theorem kind (K (K I)) a elems concl
   | smart_theorem kind (SOME loc) a elems concl =
@@ -2410,7 +2407,7 @@
   in (propss, activate) end;
 
 fun prep_propp propss = propss |> map (fn ((name, _), props) =>
-  map (rpair ([], [])) props);
+  (("", []), map (rpair ([], [])) props));
 
 fun goal_name thy kind target propss =
     kind ^ Proof.goal_names (Option.map (extern thy) target) ""
@@ -2422,41 +2419,32 @@
   let
     val thy_ctxt = ProofContext.init thy;
     val (propss, activate) = prep_global_registration (prfx, atts) expr insts thy;
+    val kind = goal_name thy "interpretation" NONE propss;
     fun after_qed (goal_ctxt, raw_results) _ =
       activate (map (ProofContext.export_plain goal_ctxt thy_ctxt) raw_results);
-  in
-    Proof.generic_goal
-      (ProofContext.bind_propp_schematic_i #> Proof.auto_fix)
-      (goal_name thy "interpretation" NONE propss)
-      (K (K Seq.single), after_qed) (prep_propp propss) (Proof.init thy_ctxt)
-  end;
+  in Proof.theorem_i kind after_qed NONE ("", []) (prep_propp propss) thy_ctxt end;
 
 fun interpretation_in_locale (raw_target, expr) thy =
   let
-    val thy_ctxt = ProofContext.init thy;
     val target = intern thy raw_target;
     val (propss, activate) = prep_registration_in_locale target expr thy;
-    val (_, (target_view, _), target_ctxt, _, propp) =
-      cert_context_statement (SOME target) [] (prep_propp propss) thy_ctxt;
-    val target_ctxt' = target_ctxt |> ProofContext.add_view thy_ctxt target_view;
-    fun after_qed (goal_ctxt, raw_results) _ =
-      activate (map (ProofContext.export_plain goal_ctxt target_ctxt') raw_results);
+    val kind = goal_name thy "interpretation" (SOME target) propss;
+    fun after_qed ((goal_ctxt, locale_ctxt), raw_results) _ =
+      activate (map (ProofContext.export_plain goal_ctxt locale_ctxt) raw_results);
+  in theorem_in_locale_no_target kind after_qed target ("", []) [] (prep_propp propss) thy end;
+
+fun interpret (prfx, atts) expr insts int state =
+  let
+    val ctxt = Proof.context_of state;
+    val (propss, activate) = prep_local_registration (prfx, atts) expr insts ctxt;
+    val kind = goal_name (Proof.theory_of state) "interpret" NONE propss;
+    fun after_qed (_, raw_results) _ =
+      Proof.map_context (K (ctxt |> activate raw_results))
+      #> Proof.put_facts NONE
+      #> Seq.single;
   in
-    Proof.generic_goal 
-      (ProofContext.bind_propp_schematic_i #> Proof.auto_fix)
-      (goal_name thy "interpretation" (SOME target) propss)
-      (K (K Seq.single), after_qed) propp (Proof.init target_ctxt')
-  end;
-
-fun interpret (prfx, atts) expr insts _ state =
-  let
-    val (propss, activate) =
-      prep_local_registration (prfx, atts) expr insts (Proof.context_of state);
-    fun after_qed (_, raw_results) _ = Seq.single o Proof.map_context (activate raw_results);
-  in
-    Proof.generic_goal ProofContext.bind_propp_i
-      (goal_name (Proof.theory_of state) "interpret" NONE propss)
-      (after_qed, K (K I)) (prep_propp propss) state
+    Proof.local_goal (ProofDisplay.print_results int) (K I) ProofContext.bind_propp_i
+      kind after_qed (prep_propp propss) state
   end;
 
 end;