src/Pure/Isar/expression.ML
changeset 54876 8fab871a2a6f
parent 54875 b370e1622e41
child 54877 0a9337337277
     1.1 --- a/src/Pure/Isar/expression.ML	Sun Dec 29 23:21:11 2013 +0100
     1.2 +++ b/src/Pure/Isar/expression.ML	Sun Dec 29 23:21:12 2013 +0100
     1.3 @@ -904,15 +904,9 @@
     1.4    end;
     1.5    
     1.6  fun gen_sublocale_global prep_expr prep_loc prep_prop prep_attr before_exit raw_locale expression raw_eqns thy =
     1.7 -  let
     1.8 -    val locale = prep_loc thy raw_locale;
     1.9 -    val add_dependency_global = Proof_Context.background_theory ooo Locale.add_dependency locale;
    1.10 -  in
    1.11 -    thy
    1.12 -    |> Named_Target.init before_exit locale
    1.13 -    |> generic_interpretation prep_expr prep_prop prep_attr Element.witness_proof_eqs
    1.14 -        Local_Theory.notes_kind add_dependency_global expression raw_eqns
    1.15 -  end;
    1.16 +  thy
    1.17 +  |> Named_Target.init before_exit (prep_loc thy raw_locale)
    1.18 +  |> gen_sublocale prep_expr prep_prop prep_attr expression raw_eqns
    1.19  
    1.20  in
    1.21