src/Pure/Isar/isar_syn.ML
changeset 61669 27ca6147e3b3
parent 61654 4a28eec739e9
child 61670 301e0b4ecd45
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Sat Nov 14 08:45:51 2015 +0100
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Sat Nov 14 08:45:51 2015 +0100
     1.3 @@ -412,21 +412,21 @@
     1.4      "prove sublocale relation between a locale and a locale expression"
     1.5      ((Parse.position Parse.xname --| (@{keyword "\<subseteq>"} || @{keyword "<"}) --
     1.6        interpretation_args >> (fn (loc, (expr, equations)) =>
     1.7 -        Toplevel.theory_to_proof (Expression.sublocale_global_cmd loc expr equations)))
     1.8 +        Toplevel.theory_to_proof (Interpretation.sublocale_global_cmd loc expr equations)))
     1.9      || interpretation_args >> (fn (expr, equations) =>
    1.10 -        Toplevel.local_theory_to_proof NONE NONE (Expression.sublocale_cmd expr equations)));
    1.11 +        Toplevel.local_theory_to_proof NONE NONE (Interpretation.sublocale_cmd expr equations)));
    1.12  
    1.13  val _ =
    1.14    Outer_Syntax.command @{command_keyword interpretation}
    1.15      "prove interpretation of locale expression in local theory"
    1.16      (interpretation_args >> (fn (expr, equations) =>
    1.17 -      Toplevel.local_theory_to_proof NONE NONE (Expression.interpretation_cmd expr equations)));
    1.18 +      Toplevel.local_theory_to_proof NONE NONE (Interpretation.interpretation_cmd expr equations)));
    1.19  
    1.20  val _ =
    1.21    Outer_Syntax.command @{command_keyword interpret}
    1.22      "prove interpretation of locale expression in proof context"
    1.23      (interpretation_args >> (fn (expr, equations) =>
    1.24 -      Toplevel.proof' (Expression.interpret_cmd expr equations)));
    1.25 +      Toplevel.proof' (Interpretation.interpret_cmd expr equations)));
    1.26  
    1.27  
    1.28  (* classes *)