more precise Local_Defs.expand wrt. *local* prems only;

--- 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 *)