misc tuning;
authorwenzelm
Sat Nov 05 22:01:19 2011 +0100 (2011-11-05 ago)
changeset 453520b4038361a3a
parent 45351 8b1604119bc0
child 45353 68f3e073ee21
misc tuning;
src/Pure/Isar/generic_target.ML
src/Pure/Isar/named_target.ML
     1.1 --- a/src/Pure/Isar/generic_target.ML	Sat Nov 05 21:36:56 2011 +0100
     1.2 +++ b/src/Pure/Isar/generic_target.ML	Sat Nov 05 22:01:19 2011 +0100
     1.3 @@ -106,14 +106,16 @@
     1.4      (*export assumes/defines*)
     1.5      val th = Goal.norm_result raw_th;
     1.6      val (defs, th') = Local_Defs.export ctxt thy_ctxt th;
     1.7 -    val assms = map (Raw_Simplifier.rewrite_rule defs o Thm.assume)
     1.8 -      (Assumption.all_assms_of ctxt);
     1.9 +    val assms =
    1.10 +      map (Raw_Simplifier.rewrite_rule defs o Thm.assume)
    1.11 +        (Assumption.all_assms_of ctxt);
    1.12      val nprems = Thm.nprems_of th' - Thm.nprems_of th;
    1.13  
    1.14      (*export fixes*)
    1.15      val tfrees = map TFree (Thm.fold_terms Term.add_tfrees th' []);
    1.16      val frees = map Free (Thm.fold_terms Term.add_frees th' []);
    1.17 -    val (th'' :: vs) = (th' :: map (Drule.mk_term o cert) (map Logic.mk_type tfrees @ frees))
    1.18 +    val (th'' :: vs) =
    1.19 +      (th' :: map (Drule.mk_term o cert) (map Logic.mk_type tfrees @ frees))
    1.20        |> Variable.export ctxt thy_ctxt
    1.21        |> Drule.zero_var_indexes_list;
    1.22  
    1.23 @@ -183,6 +185,7 @@
    1.24    end;
    1.25  
    1.26  
    1.27 +
    1.28  (** primitive theory operations **)
    1.29  
    1.30  fun theory_declaration decl lthy =
     2.1 --- a/src/Pure/Isar/named_target.ML	Sat Nov 05 21:36:56 2011 +0100
     2.2 +++ b/src/Pure/Isar/named_target.ML	Sat Nov 05 22:01:19 2011 +0100
     2.3 @@ -65,46 +65,45 @@
     2.4  
     2.5  (* consts in locales *)
     2.6  
     2.7 -fun locale_const (Target {target, is_class, ...}) (prmode as (mode, _)) ((b, mx), rhs) phi =
     2.8 -  let
     2.9 -    val b' = Morphism.binding phi b;
    2.10 -    val rhs' = Morphism.term phi rhs;
    2.11 -    val arg = (b', Term.close_schematic_term rhs');
    2.12 -    val same_shape = Term.aconv_untyped (rhs, rhs');
    2.13 -    (* FIXME workaround based on educated guess *)
    2.14 -    val prefix' = Binding.prefix_of b';
    2.15 -    val is_canonical_class = is_class andalso
    2.16 -      (Binding.eq_name (b, b')
    2.17 -        andalso not (null prefix')
    2.18 -        andalso List.last prefix' = (Class.class_prefix target, false)
    2.19 -      orelse same_shape);
    2.20 -  in
    2.21 -    not is_canonical_class ?
    2.22 -      (Context.mapping_result
    2.23 -        (Sign.add_abbrev Print_Mode.internal arg)
    2.24 -        (Proof_Context.add_abbrev Print_Mode.internal arg)
    2.25 -      #-> (fn (lhs' as Const (d, _), _) =>
    2.26 -          same_shape ?
    2.27 -            (Context.mapping
    2.28 -              (Sign.revert_abbrev mode d) (Proof_Context.revert_abbrev mode d) #>
    2.29 -             Morphism.form (Proof_Context.target_notation true prmode [(lhs', mx)]))))
    2.30 -  end;
    2.31 +fun locale_const (ta as Target {target, is_class, ...}) (prmode as (mode, _)) ((b, mx), rhs) =
    2.32 +  locale_declaration target true (fn phi =>
    2.33 +    let
    2.34 +      val b' = Morphism.binding phi b;
    2.35 +      val rhs' = Morphism.term phi rhs;
    2.36 +      val arg = (b', Term.close_schematic_term rhs');
    2.37 +      val same_shape = Term.aconv_untyped (rhs, rhs');
    2.38  
    2.39 -fun locale_const_declaration (ta as Target {target, ...}) prmode arg =
    2.40 -  locale_declaration target true (locale_const ta prmode arg);
    2.41 +      (* FIXME workaround based on educated guess *)
    2.42 +      val prefix' = Binding.prefix_of b';
    2.43 +      val is_canonical_class = is_class andalso
    2.44 +        (Binding.eq_name (b, b')
    2.45 +          andalso not (null prefix')
    2.46 +          andalso List.last prefix' = (Class.class_prefix target, false)
    2.47 +        orelse same_shape);
    2.48 +    in
    2.49 +      not is_canonical_class ?
    2.50 +        (Context.mapping_result
    2.51 +          (Sign.add_abbrev Print_Mode.internal arg)
    2.52 +          (Proof_Context.add_abbrev Print_Mode.internal arg)
    2.53 +        #-> (fn (lhs' as Const (d, _), _) =>
    2.54 +            same_shape ?
    2.55 +              (Context.mapping
    2.56 +                (Sign.revert_abbrev mode d) (Proof_Context.revert_abbrev mode d) #>
    2.57 +               Morphism.form (Proof_Context.target_notation true prmode [(lhs', mx)]))))
    2.58 +    end);
    2.59  
    2.60  
    2.61  (* define *)
    2.62  
    2.63  fun locale_foundation ta (((b, U), mx), (b_def, rhs)) (type_params, term_params) =
    2.64    Generic_Target.theory_foundation (((b, U), NoSyn), (b_def, rhs)) (type_params, term_params)
    2.65 -  #-> (fn (lhs, def) => locale_const_declaration ta Syntax.mode_default ((b, mx), lhs)
    2.66 +  #-> (fn (lhs, def) => locale_const ta Syntax.mode_default ((b, mx), lhs)
    2.67      #> pair (lhs, def))
    2.68  
    2.69  fun class_foundation (ta as Target {target, ...})
    2.70      (((b, U), mx), (b_def, rhs)) (type_params, term_params) =
    2.71    Generic_Target.theory_foundation (((b, U), NoSyn), (b_def, rhs)) (type_params, term_params)
    2.72 -  #-> (fn (lhs, def) => locale_const_declaration ta Syntax.mode_default ((b, NoSyn), lhs)
    2.73 +  #-> (fn (lhs, def) => locale_const ta Syntax.mode_default ((b, NoSyn), lhs)
    2.74      #> Class.const target ((b, mx), (type_params, lhs))
    2.75      #> pair (lhs, def))
    2.76  
    2.77 @@ -137,7 +136,7 @@
    2.78  fun locale_abbrev ta prmode ((b, mx), t) xs =
    2.79    Local_Theory.background_theory_result
    2.80      (Sign.add_abbrev Print_Mode.internal (b, t)) #->
    2.81 -      (fn (lhs, _) => locale_const_declaration ta prmode
    2.82 +      (fn (lhs, _) => locale_const ta prmode
    2.83          ((b, mx), Term.list_comb (Logic.unvarify_global lhs, xs)));
    2.84  
    2.85  fun target_abbrev (ta as Target {target, is_locale, is_class, ...})
    2.86 @@ -204,7 +203,8 @@
    2.87  
    2.88  fun reinit lthy =
    2.89    (case Data.get lthy of
    2.90 -    SOME (Target {target, before_exit, ...}) => init before_exit target o Local_Theory.exit_global
    2.91 +    SOME (Target {target, before_exit, ...}) =>
    2.92 +      init before_exit target o Local_Theory.exit_global
    2.93    | NONE => error "Not in a named target");
    2.94  
    2.95  fun context_cmd "-" thy = init I "" thy