# HG changeset patch
# User wenzelm
# Date 1333200589 -7200
# Node ID b61a11dea74c690391a7bd96f773a4c4f3780819
# Parent  973ab740a25d2bd1983507ffc0eeb3b518029c0c
more precise Local_Defs.expand wrt. *local* prems only;

diff -r 973ab740a25d -r b61a11dea74c src/Pure/Isar/local_defs.ML
--- a/src/Pure/Isar/local_defs.ML	Sat Mar 31 15:21:35 2012 +0200
+++ b/src/Pure/Isar/local_defs.ML	Sat Mar 31 15:29:49 2012 +0200
@@ -137,7 +137,7 @@
   let
     val exp = Assumption.export false inner outer;
     val exp_term = Assumption.export_term inner outer;
-    val prems = Assumption.all_prems_of inner;
+    val prems = Assumption.local_prems_of inner outer;
   in
     fn th =>
       let
@@ -192,6 +192,7 @@
   trans_props ctxt [th, Thm.symmetric (Raw_Simplifier.rewrite true defs ct)];
 
 
+
 (** defived definitions **)
 
 (* transformation rules *)