# HG changeset patch
# User wenzelm
# Date 1565774067 -7200
# Node ID 9b3610fe74d62d9444fd14323219e6b866aba15e
# Parent  095e6459d3dac028ae7f2b272702305243d0b18a
treat simproc results as atomic -- more compact proof terms;

diff -r 095e6459d3da -r 9b3610fe74d6 src/Pure/raw_simplifier.ML
--- a/src/Pure/raw_simplifier.ML	Tue Aug 13 21:52:08 2019 +0200
+++ b/src/Pure/raw_simplifier.ML	Wed Aug 14 11:14:27 2019 +0200
@@ -905,10 +905,13 @@
 (* mk_procrule *)
 
 fun mk_procrule ctxt thm =
-  let val (prems, lhs, elhs, rhs, _) = decomp_simp thm in
+  let
+    val (prems, lhs, elhs, rhs, _) = decomp_simp thm
+    val thm' = Thm.close_derivation \<^here> thm;
+  in
     if rewrite_rule_extra_vars prems lhs rhs
     then (cond_warning ctxt (fn () => print_thm ctxt "Extra vars on rhs:" ("", thm)); [])
-    else [mk_rrule2 {thm = thm, name = "", lhs = lhs, elhs = elhs, perm = false}]
+    else [mk_rrule2 {thm = thm', name = "", lhs = lhs, elhs = elhs, perm = false}]
   end;