diff -r e89dde5f365c -r 829e684b02ef src/FOL/ex/NewLocaleSetup.thy
--- a/src/FOL/ex/NewLocaleSetup.thy	Wed Dec 03 15:27:41 2008 +0100
+++ b/src/FOL/ex/NewLocaleSetup.thy	Fri Dec 05 11:26:07 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      FOL/ex/NewLocaleSetup.thy
-    ID:         $Id$
     Author:     Clemens Ballarin, TU Muenchen
 
 Testing environment for locale expressions --- experimental.
@@ -40,6 +39,13 @@
    Toplevel.unknown_theory o Toplevel.keep (fn state =>
      NewLocale.print_locale (Toplevel.theory_of state) show_facts name))));
 
+val _ =
+  OuterSyntax.command "interpretation"
+    "prove and register interpretation of locale expression in theory" K.thy_goal
+    (P.!!! Expression.parse_expression
+        >> (fn expr => Toplevel.print o
+            Toplevel.theory_to_proof (Expression.interpretation_cmd expr)));
+
 end
 
 *}