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