src/Pure/Isar/expression.ML
changeset 52153 f5773a46cf05
parent 52148 893b15200ec1
child 52230 1105b3b5aa77
     1.1 --- a/src/Pure/Isar/expression.ML	Sun May 26 19:45:54 2013 +0200
     1.2 +++ b/src/Pure/Isar/expression.ML	Sun May 26 19:45:54 2013 +0200
     1.3 @@ -882,7 +882,7 @@
     1.4    then 
     1.5      lthy
     1.6      |> generic_interpretation prep_expr prep_prop prep_attr Element.witness_proof_eqs
     1.7 -        Local_Theory.notes_kind Local_Theory.add_registration expression raw_eqns
     1.8 +        Local_Theory.notes_kind Generic_Target.theory_registration expression raw_eqns
     1.9    else
    1.10      lthy
    1.11      |> generic_interpretation prep_expr prep_prop prep_attr Element.witness_proof_eqs
    1.12 @@ -895,7 +895,7 @@
    1.13    in
    1.14      lthy
    1.15      |> generic_interpretation prep_expr prep_prop prep_attr Element.witness_proof_eqs
    1.16 -        Local_Theory.notes_kind (Local_Theory.add_dependency locale) expression raw_eqns
    1.17 +        Local_Theory.notes_kind (Generic_Target.locale_dependency locale) expression raw_eqns
    1.18    end;
    1.19    
    1.20  fun gen_sublocale_global prep_expr prep_loc prep_prop prep_attr before_exit raw_locale expression raw_eqns thy =
    1.21 @@ -915,8 +915,8 @@
    1.22    let
    1.23      val _ = Local_Theory.assert_bottom true lthy;
    1.24      val target = Named_Target.the_name lthy;
    1.25 -    val subscribe = if target = "" then Local_Theory.add_registration
    1.26 -      else Local_Theory.add_dependency target;
    1.27 +    val subscribe = if target = "" then Generic_Target.theory_registration
    1.28 +      else Generic_Target.locale_dependency target;
    1.29    in
    1.30      lthy
    1.31      |> generic_interpretation cert_goal_expression (K I) (K I) Element.witness_proof_eqs