src/Pure/Isar/expression.ML
changeset 28902 2019bcc9d8bf
parent 28898 530c7d28a962
child 28903 b3fc3a62247a
     1.1 --- a/src/Pure/Isar/expression.ML	Fri Nov 28 11:55:46 2008 +0100
     1.2 +++ b/src/Pure/Isar/expression.ML	Fri Nov 28 12:26:14 2008 +0100
     1.3 @@ -19,19 +19,20 @@
     1.4      Proof.context -> (term * term list) list list * Proof.context;
     1.5  
     1.6    (* Declaring locales *)
     1.7 -  val add_locale: string -> bstring -> expression -> Element.context list -> theory ->
     1.8 +  val add_locale_cmd: string -> bstring -> expression -> Element.context list -> theory ->
     1.9      string * Proof.context
    1.10 -  val add_locale_i: string -> bstring -> expression_i -> Element.context_i list -> theory ->
    1.11 +  val add_locale: string -> bstring -> expression_i -> Element.context_i list -> theory ->
    1.12      string * Proof.context
    1.13  
    1.14    (* Interpretation *)
    1.15 -  val sublocale: (thm list list -> Proof.context -> Proof.context) ->
    1.16 +  val sublocale_cmd: (thm list list -> Proof.context -> Proof.context) ->
    1.17      string -> expression -> theory -> Proof.state;
    1.18 -  val sublocale_i: (thm list list -> Proof.context -> Proof.context) ->
    1.19 +  val sublocale: (thm list list -> Proof.context -> Proof.context) ->
    1.20      string -> expression_i -> theory -> Proof.state;
    1.21  
    1.22    (* Debugging and development *)
    1.23    val parse_expression: OuterParse.token list -> expression * OuterParse.token list
    1.24 +    (* FIXME to spec_parse.ML *)
    1.25  end;
    1.26  
    1.27  
    1.28 @@ -776,8 +777,8 @@
    1.29  
    1.30  in
    1.31  
    1.32 -val add_locale = gen_add_locale read_declaration;
    1.33 -val add_locale_i = gen_add_locale cert_declaration;
    1.34 +val add_locale_cmd = gen_add_locale read_declaration;
    1.35 +val add_locale = gen_add_locale cert_declaration;
    1.36  
    1.37  end;
    1.38  
    1.39 @@ -796,19 +797,19 @@
    1.40  
    1.41  local
    1.42  
    1.43 -fun gen_sublocale prep_expr
    1.44 -    after_qed target expression thy =
    1.45 +fun gen_sublocale prep_expr intern
    1.46 +    after_qed raw_target expression thy =
    1.47    let
    1.48 +    val target = intern thy raw_target;
    1.49      val target_ctxt = NewLocale.init target thy;
    1.50 -    val target' = NewLocale.intern thy target;
    1.51  
    1.52      val ((propss, deps, export'), goal_ctxt) = prep_expr expression target_ctxt;
    1.53      
    1.54 -    fun store_dep target ((name, morph), thms) =
    1.55 +    fun store_dep ((name, morph), thms) =
    1.56        NewLocale.add_dependency target (name, morph $> Element.satisfy_morphism thms $> export');
    1.57  
    1.58      fun after_qed' results =
    1.59 -      fold (store_dep target') (deps ~~ prep_result propss results) #>
    1.60 +      fold store_dep (deps ~~ prep_result propss results) #>
    1.61        after_qed results;
    1.62  
    1.63    in
    1.64 @@ -819,8 +820,8 @@
    1.65  
    1.66  in
    1.67  
    1.68 -fun sublocale x = gen_sublocale read_goal_expression x;
    1.69 -fun sublocale_i x = gen_sublocale cert_goal_expression x;
    1.70 +fun sublocale_cmd x = gen_sublocale read_goal_expression NewLocale.intern x;
    1.71 +fun sublocale x = gen_sublocale cert_goal_expression (K I) x;
    1.72  
    1.73  end;
    1.74