# HG changeset patch
# User haftmann
# Date 1388355672 -3600
# Node ID 8fab871a2a6fd26d98e12ee944f2bcffd495ae6c
# Parent  b370e1622e411ebaade9febaeade5f025c6c782b
more succint formulation of special case

diff -r b370e1622e41 -r 8fab871a2a6f src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Sun Dec 29 23:21:11 2013 +0100
+++ b/src/Pure/Isar/expression.ML	Sun Dec 29 23:21:12 2013 +0100
@@ -904,15 +904,9 @@
   end;
   
 fun gen_sublocale_global prep_expr prep_loc prep_prop prep_attr before_exit raw_locale expression raw_eqns thy =
-  let
-    val locale = prep_loc thy raw_locale;
-    val add_dependency_global = Proof_Context.background_theory ooo Locale.add_dependency locale;
-  in
-    thy
-    |> Named_Target.init before_exit locale
-    |> generic_interpretation prep_expr prep_prop prep_attr Element.witness_proof_eqs
-        Local_Theory.notes_kind add_dependency_global expression raw_eqns
-  end;
+  thy
+  |> Named_Target.init before_exit (prep_loc thy raw_locale)
+  |> gen_sublocale prep_expr prep_prop prep_attr expression raw_eqns
 
 in