adjusted locale signature to *_cmd convention
authorhaftmann
Mon Nov 17 17:00:22 2008 +0100 (2008-11-17)
changeset 2882095dd21624c6c
parent 28819 daca685d7bb7
child 28821 78a6ed46ad04
adjusted locale signature to *_cmd convention
src/HOL/Statespace/state_space.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/specification.ML
     1.1 --- a/src/HOL/Statespace/state_space.ML	Mon Nov 17 17:00:21 2008 +0100
     1.2 +++ b/src/HOL/Statespace/state_space.ML	Mon Nov 17 17:00:22 2008 +0100
     1.3 @@ -311,7 +311,7 @@
     1.4                        ([]))])];
     1.5  
     1.6    in thy
     1.7 -     |> Locale.add_locale_i "" name vars [assumes]
     1.8 +     |> Locale.add_locale "" name vars [assumes]
     1.9       ||> ProofContext.theory_of
    1.10       ||> interprete_parent name dist_thm_full_name parent_expr
    1.11       |> #2
    1.12 @@ -457,11 +457,11 @@
    1.13             (suffix namespaceN name) nameT parents_expr
    1.14             (map fst parent_comps) (map fst components)
    1.15       |> Context.theory_map (add_statespace full_name args parents components [])
    1.16 -     |> Locale.add_locale_i "" (suffix valuetypesN name) (Locale.Merge locs)
    1.17 +     |> Locale.add_locale "" (suffix valuetypesN name) (Locale.Merge locs)
    1.18              [Element.Constrains constrains]
    1.19       |> ProofContext.theory_of o #2
    1.20       |> fold interprete_parent_valuetypes parents
    1.21 -     |> Locale.add_locale "" name
    1.22 +     |> Locale.add_locale_cmd name
    1.23                (Locale.Merge [Locale.Locale (suffix namespaceN full_name)
    1.24                              ,Locale.Locale (suffix valuetypesN full_name)]) fixestate
    1.25       |> ProofContext.theory_of o #2
     2.1 --- a/src/Pure/Isar/isar_syn.ML	Mon Nov 17 17:00:21 2008 +0100
     2.2 +++ b/src/Pure/Isar/isar_syn.ML	Mon Nov 17 17:00:22 2008 +0100
     2.3 @@ -394,7 +394,7 @@
     2.4      (P.name -- Scan.optional (P.$$$ "=" |-- P.!!! locale_val) (Locale.empty, []) -- P.opt_begin
     2.5        >> (fn ((name, (expr, elems)), begin) =>
     2.6            (begin ? Toplevel.print) o Toplevel.begin_local_theory begin
     2.7 -            (Locale.add_locale "" name expr elems #-> TheoryTarget.begin)));
     2.8 +            (Locale.add_locale_cmd name expr elems #-> TheoryTarget.begin)));
     2.9  
    2.10  val opt_prefix = Scan.optional (P.binding --| P.$$$ ":") Name.no_binding;
    2.11  
    2.12 @@ -406,7 +406,7 @@
    2.13        opt_prefix  -- SpecParse.locale_expr -- SpecParse.locale_insts
    2.14          >> (fn ((name, expr), insts) => Toplevel.print o
    2.15              Toplevel.theory_to_proof
    2.16 -              (Locale.interpretation I (true, Name.name_of name) expr insts #> snd)));
    2.17 +              (Locale.interpretation_cmd (Name.name_of name) expr insts)));
    2.18  
    2.19  val _ =
    2.20    OuterSyntax.command "interpret"
    2.21 @@ -415,7 +415,7 @@
    2.22      (opt_prefix -- SpecParse.locale_expr -- SpecParse.locale_insts
    2.23        >> (fn ((name, expr), insts) => Toplevel.print o
    2.24            Toplevel.proof'
    2.25 -            (fn int => Locale.interpret Seq.single (true, Name.name_of name) expr insts int #> snd)));
    2.26 +            (fn int => Locale.interpret_cmd (Name.name_of name) expr insts int)));
    2.27  
    2.28  
    2.29  (* classes *)
     3.1 --- a/src/Pure/Isar/specification.ML	Mon Nov 17 17:00:21 2008 +0100
     3.2 +++ b/src/Pure/Isar/specification.ML	Mon Nov 17 17:00:22 2008 +0100
     3.3 @@ -368,7 +368,7 @@
     3.4  in
     3.5  
     3.6  val theorem = gen_theorem (K I) Locale.cert_context_statement;
     3.7 -val theorem_cmd = gen_theorem Attrib.intern_src Locale.read_context_statement_i;
     3.8 +val theorem_cmd = gen_theorem Attrib.intern_src Locale.read_context_statement;
     3.9  
    3.10  fun add_theorem_hook f = TheoremHook.map (cons (f, stamp ()));
    3.11