# HG changeset patch
# User wenzelm
# Date 1684444865 -7200
# Node ID 073826f50e146ec7f2fbc28d3cc8f5e522f7782b
# Parent  b8dfaba8394f0536f97deddb69ac31cb10fad6a4
tuned;

diff -r b8dfaba8394f -r 073826f50e14 src/Pure/Isar/spec_rules.ML
--- a/src/Pure/Isar/spec_rules.ML	Thu May 18 23:20:41 2023 +0200
+++ b/src/Pure/Isar/spec_rules.ML	Thu May 18 23:21:05 2023 +0200
@@ -158,7 +158,10 @@
 (* add *)
 
 fun add b rough_classification terms rules lthy =
-  let val thms0 = map Thm.trim_context (map (Drule.mk_term o Thm.cterm_of lthy) terms @ rules) in
+  let
+    val n = length terms;
+    val thms0 = map Thm.trim_context (map (Drule.mk_term o Thm.cterm_of lthy) terms @ rules);
+  in
     lthy |> Local_Theory.declaration {syntax = false, pervasive = true}
       (fn phi => fn context =>
         let
@@ -166,8 +169,7 @@
           val pos = Position.thread_data ();
           val name = Name_Space.full_name (Name_Space.naming_of context) (Morphism.binding psi b);
           val (terms', rules') =
-            Morphism.fact psi thms0
-            |> chop (length terms)
+            chop n (Morphism.fact psi thms0)
             |>> map (Thm.term_of o Drule.dest_term);
         in
           context |> (Data.map o Item_Net.update)