src/Pure/Isar/named_target.ML
changeset 45352 0b4038361a3a
parent 45311 ca9e66c523a2
child 45353 68f3e073ee21
     1.1 --- a/src/Pure/Isar/named_target.ML	Sat Nov 05 21:36:56 2011 +0100
     1.2 +++ b/src/Pure/Isar/named_target.ML	Sat Nov 05 22:01:19 2011 +0100
     1.3 @@ -65,46 +65,45 @@
     1.4  
     1.5  (* consts in locales *)
     1.6  
     1.7 -fun locale_const (Target {target, is_class, ...}) (prmode as (mode, _)) ((b, mx), rhs) phi =
     1.8 -  let
     1.9 -    val b' = Morphism.binding phi b;
    1.10 -    val rhs' = Morphism.term phi rhs;
    1.11 -    val arg = (b', Term.close_schematic_term rhs');
    1.12 -    val same_shape = Term.aconv_untyped (rhs, rhs');
    1.13 -    (* FIXME workaround based on educated guess *)
    1.14 -    val prefix' = Binding.prefix_of b';
    1.15 -    val is_canonical_class = is_class andalso
    1.16 -      (Binding.eq_name (b, b')
    1.17 -        andalso not (null prefix')
    1.18 -        andalso List.last prefix' = (Class.class_prefix target, false)
    1.19 -      orelse same_shape);
    1.20 -  in
    1.21 -    not is_canonical_class ?
    1.22 -      (Context.mapping_result
    1.23 -        (Sign.add_abbrev Print_Mode.internal arg)
    1.24 -        (Proof_Context.add_abbrev Print_Mode.internal arg)
    1.25 -      #-> (fn (lhs' as Const (d, _), _) =>
    1.26 -          same_shape ?
    1.27 -            (Context.mapping
    1.28 -              (Sign.revert_abbrev mode d) (Proof_Context.revert_abbrev mode d) #>
    1.29 -             Morphism.form (Proof_Context.target_notation true prmode [(lhs', mx)]))))
    1.30 -  end;
    1.31 +fun locale_const (ta as Target {target, is_class, ...}) (prmode as (mode, _)) ((b, mx), rhs) =
    1.32 +  locale_declaration target true (fn phi =>
    1.33 +    let
    1.34 +      val b' = Morphism.binding phi b;
    1.35 +      val rhs' = Morphism.term phi rhs;
    1.36 +      val arg = (b', Term.close_schematic_term rhs');
    1.37 +      val same_shape = Term.aconv_untyped (rhs, rhs');
    1.38  
    1.39 -fun locale_const_declaration (ta as Target {target, ...}) prmode arg =
    1.40 -  locale_declaration target true (locale_const ta prmode arg);
    1.41 +      (* FIXME workaround based on educated guess *)
    1.42 +      val prefix' = Binding.prefix_of b';
    1.43 +      val is_canonical_class = is_class andalso
    1.44 +        (Binding.eq_name (b, b')
    1.45 +          andalso not (null prefix')
    1.46 +          andalso List.last prefix' = (Class.class_prefix target, false)
    1.47 +        orelse same_shape);
    1.48 +    in
    1.49 +      not is_canonical_class ?
    1.50 +        (Context.mapping_result
    1.51 +          (Sign.add_abbrev Print_Mode.internal arg)
    1.52 +          (Proof_Context.add_abbrev Print_Mode.internal arg)
    1.53 +        #-> (fn (lhs' as Const (d, _), _) =>
    1.54 +            same_shape ?
    1.55 +              (Context.mapping
    1.56 +                (Sign.revert_abbrev mode d) (Proof_Context.revert_abbrev mode d) #>
    1.57 +               Morphism.form (Proof_Context.target_notation true prmode [(lhs', mx)]))))
    1.58 +    end);
    1.59  
    1.60  
    1.61  (* define *)
    1.62  
    1.63  fun locale_foundation ta (((b, U), mx), (b_def, rhs)) (type_params, term_params) =
    1.64    Generic_Target.theory_foundation (((b, U), NoSyn), (b_def, rhs)) (type_params, term_params)
    1.65 -  #-> (fn (lhs, def) => locale_const_declaration ta Syntax.mode_default ((b, mx), lhs)
    1.66 +  #-> (fn (lhs, def) => locale_const ta Syntax.mode_default ((b, mx), lhs)
    1.67      #> pair (lhs, def))
    1.68  
    1.69  fun class_foundation (ta as Target {target, ...})
    1.70      (((b, U), mx), (b_def, rhs)) (type_params, term_params) =
    1.71    Generic_Target.theory_foundation (((b, U), NoSyn), (b_def, rhs)) (type_params, term_params)
    1.72 -  #-> (fn (lhs, def) => locale_const_declaration ta Syntax.mode_default ((b, NoSyn), lhs)
    1.73 +  #-> (fn (lhs, def) => locale_const ta Syntax.mode_default ((b, NoSyn), lhs)
    1.74      #> Class.const target ((b, mx), (type_params, lhs))
    1.75      #> pair (lhs, def))
    1.76  
    1.77 @@ -137,7 +136,7 @@
    1.78  fun locale_abbrev ta prmode ((b, mx), t) xs =
    1.79    Local_Theory.background_theory_result
    1.80      (Sign.add_abbrev Print_Mode.internal (b, t)) #->
    1.81 -      (fn (lhs, _) => locale_const_declaration ta prmode
    1.82 +      (fn (lhs, _) => locale_const ta prmode
    1.83          ((b, mx), Term.list_comb (Logic.unvarify_global lhs, xs)));
    1.84  
    1.85  fun target_abbrev (ta as Target {target, is_locale, is_class, ...})
    1.86 @@ -204,7 +203,8 @@
    1.87  
    1.88  fun reinit lthy =
    1.89    (case Data.get lthy of
    1.90 -    SOME (Target {target, before_exit, ...}) => init before_exit target o Local_Theory.exit_global
    1.91 +    SOME (Target {target, before_exit, ...}) =>
    1.92 +      init before_exit target o Local_Theory.exit_global
    1.93    | NONE => error "Not in a named target");
    1.94  
    1.95  fun context_cmd "-" thy = init I "" thy