--- a/src/Pure/Isar/isar_syn.ML Wed Dec 03 15:26:46 2008 +0100
+++ b/src/Pure/Isar/isar_syn.ML Wed Dec 03 15:27:41 2008 +0100
@@ -403,7 +403,7 @@
"prove sublocale relation between a locale and a locale expression" K.thy_goal
(P.xname --| (P.$$$ "\\<subseteq>" || P.$$$ "<") -- P.!!! Expression.parse_expression
>> (fn (loc, expr) =>
- Toplevel.print o (Toplevel.theory_to_proof (Expression.sublocale_cmd (K I) loc expr))));
+ Toplevel.print o (Toplevel.theory_to_proof (Expression.sublocale_cmd loc expr))));
val _ =
OuterSyntax.command "interpretation"