# HG changeset patch
# User wenzelm
# Date 1684160303 -7200
# Node ID 2d60172c0ade49ff67d41aff3f5b1f7477a78bbc
# Parent  bb60ea7318d63d55675c86e0054a89a66425d190
clarified stored thm: result from notes;
tuned;

diff -r bb60ea7318d6 -r 2d60172c0ade src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Mon May 15 15:14:19 2023 +0200
+++ b/src/Pure/Isar/specification.ML	Mon May 15 16:18:23 2023 +0200
@@ -259,21 +259,19 @@
     val ((lhs, (_, raw_th)), lthy2) = lthy
       |> Local_Theory.define_internal ((b, mx), ((Binding.suffix_name "_raw" name, []), rhs));
 
-    val th = prove lthy2 raw_th;
-    val lthy3 = lthy2 |> Spec_Rules.add name Spec_Rules.equational [lhs] [th];
+    val ([(def_name, [th])], lthy3) = lthy2
+      |> Local_Theory.notes [((name, atts), [([prove lthy2 raw_th], [])])];
 
-    val ([(def_name, [th'])], lthy4) = lthy3
-      |> Local_Theory.notes [((name, atts), [([th], [])])];
+    val lthy4 = lthy3
+      |> Spec_Rules.add name Spec_Rules.equational [lhs] [th]
+      |> Code.declare_default_eqns [(th, true)];
 
-    val lthy5 = lthy4
-      |> Code.declare_default_eqns [(th', true)];
-
-    val lhs' = Morphism.term (Local_Theory.target_morphism lthy5) lhs;
+    val lhs' = Morphism.term (Local_Theory.target_morphism lthy4) lhs;
 
     val _ =
-      Proof_Display.print_consts int (Position.thread_data ()) lthy5
+      Proof_Display.print_consts int (Position.thread_data ()) lthy4
         (Frees.defined (Frees.build (Frees.add_frees lhs'))) [(x, T)];
-  in ((lhs, (def_name, th')), lthy5) end;
+  in ((lhs, (def_name, th)), lthy4) end;
 
 fun definition xs ys As B = gen_def check_spec_open (K I) xs ys As B false;
 val definition_cmd = gen_def read_spec_open Attrib.check_src;