src/Pure/Isar/isar_syn.ML

     (K.tag_proof K.prf_goal)
     (P.!!! SpecParse.locale_expression
         >> (fn expr => Toplevel.print o
             Toplevel.proof' (fn int => Expression.interpret_cmd expr int)));
 
-local
-
-val opt_prefix = Scan.optional (P.binding --| P.$$$ ":") Binding.empty;
-
-in
-
-val locale_val =
-  SpecParse.locale_expr --
-    Scan.optional (P.$$$ "+" |-- P.!!! (Scan.repeat1 SpecParse.context_element)) [] ||
-  Scan.repeat1 SpecParse.context_element >> pair Old_Locale.empty;
-
-val _ =
-  OuterSyntax.command "class_locale" "define named proof context based on classes" K.thy_decl
-    (P.name -- Scan.optional (P.$$$ "=" |-- P.!!! locale_val) (Old_Locale.empty, []) -- P.opt_begin
-      >> (fn ((name, (expr, elems)), begin) =>
-          (begin ? Toplevel.print) o Toplevel.begin_local_theory begin
-            (Old_Locale.add_locale_cmd name expr elems #-> TheoryTarget.begin)));
-
-val _ =
-  OuterSyntax.command "class_interpretation"
-    "prove and register interpretation of locale expression in theory or locale" K.thy_goal
-    (P.xname --| (P.$$$ "\\<subseteq>" || P.$$$ "<") -- P.!!! SpecParse.locale_expr
-      >> (Toplevel.print oo (Toplevel.theory_to_proof o Old_Locale.interpretation_in_locale I)) ||
-      opt_prefix  -- SpecParse.locale_expr -- SpecParse.locale_insts
-        >> (fn ((name, expr), insts) => Toplevel.print o
-            Toplevel.theory_to_proof
-              (Old_Locale.interpretation_cmd (Binding.base_name name) expr insts)));
-
-val _ =
-  OuterSyntax.command "class_interpret"
-    "prove and register interpretation of locale expression in proof context"
-    (K.tag_proof K.prf_goal)
-    (opt_prefix -- SpecParse.locale_expr -- SpecParse.locale_insts
-      >> (fn ((name, expr), insts) => Toplevel.print o
-          Toplevel.proof'
-            (fn int => Old_Locale.interpret_cmd (Binding.base_name name) expr insts int)));
-
-end;
-
 
 (* classes *)
 
 val class_val =
   SpecParse.class_expr --

       o Toplevel.keep (Class.print_classes o Toplevel.theory_of)));
 
 val _ =
   OuterSyntax.improper_command "print_locale" "print locale expression in this theory" K.diag
     (opt_bang -- P.xname >> (Toplevel.no_timing oo IsarCmd.print_locale));
-
-val _ =
-  OuterSyntax.improper_command "print_interps"
-    "print interpretations of named locale" K.diag
-    (Scan.optional (P.$$$ "!" >> K true) false -- P.xname
-      >> (Toplevel.no_timing oo uncurry IsarCmd.print_registrations));
 
 val _ =
   OuterSyntax.improper_command "print_attributes" "print attributes of this theory" K.diag
     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_attributes));