--- a/src/HOL/Record.thy Tue Feb 16 13:26:21 2010 +0100
+++ b/src/HOL/Record.thy Tue Feb 16 13:35:42 2010 +0100
@@ -425,17 +425,17 @@
"_constify" :: "id => ident" ("_")
"_constify" :: "longid => ident" ("_")
- "_field_type" :: "[ident, type] => field_type" ("(2_ ::/ _)")
+ "_field_type" :: "ident => type => field_type" ("(2_ ::/ _)")
"" :: "field_type => field_types" ("_")
- "_field_types" :: "[field_type, field_types] => field_types" ("_,/ _")
+ "_field_types" :: "field_type => field_types => field_types" ("_,/ _")
"_record_type" :: "field_types => type" ("(3'(| _ |'))")
- "_record_type_scheme" :: "[field_types, type] => type" ("(3'(| _,/ (2... ::/ _) |'))")
+ "_record_type_scheme" :: "field_types => type => type" ("(3'(| _,/ (2... ::/ _) |'))")
- "_field" :: "[ident, 'a] => field" ("(2_ =/ _)")
+ "_field" :: "ident => 'a => field" ("(2_ =/ _)")
"" :: "field => fields" ("_")
- "_fields" :: "[field, fields] => fields" ("_,/ _")
+ "_fields" :: "field => fields => fields" ("_,/ _")
"_record" :: "fields => 'a" ("(3'(| _ |'))")
- "_record_scheme" :: "[fields, 'a] => 'a" ("(3'(| _,/ (2... =/ _) |'))")
+ "_record_scheme" :: "fields => 'a => 'a" ("(3'(| _,/ (2... =/ _) |'))")
"_update_name" :: idt
"_update" :: "ident => 'a => update" ("(2_ :=/ _)")
--- a/src/HOL/Tools/record.ML Tue Feb 16 13:26:21 2010 +0100
+++ b/src/HOL/Tools/record.ML Tue Feb 16 13:35:42 2010 +0100
@@ -270,11 +270,9 @@
val Trueprop = HOLogic.mk_Trueprop;
fun All xs t = Term.list_all_free (xs, t);
-infix 9 $$;
infix 0 :== ===;
infixr 0 ==>;
-val op $$ = Term.list_comb;
val op :== = Primitive_Defs.mk_defpair;
val op === = Trueprop o HOLogic.mk_eq;
val op ==> = Logic.mk_implies;
@@ -586,9 +584,9 @@
let
val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =
Records_Data.get thy;
- val data = make_record_data records sel_upd
- equalities extinjects (Symtab.update_new (name, thm) extsplit) splits
- extfields fieldext;
+ val data =
+ make_record_data records sel_upd equalities extinjects
+ (Symtab.update_new (name, thm) extsplit) splits extfields fieldext;
in Records_Data.put data thy end;
@@ -598,9 +596,9 @@
let
val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =
Records_Data.get thy;
- val data = make_record_data records sel_upd
- equalities extinjects extsplit (Symtab.update_new (name, thmP) splits)
- extfields fieldext;
+ val data =
+ make_record_data records sel_upd equalities extinjects extsplit
+ (Symtab.update_new (name, thmP) splits) extfields fieldext;
in Records_Data.put data thy end;
val get_splits = Symtab.lookup o #splits o Records_Data.get;
@@ -619,8 +617,7 @@
val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =
Records_Data.get thy;
val data =
- make_record_data records sel_upd
- equalities extinjects extsplit splits
+ make_record_data records sel_upd equalities extinjects extsplit splits
(Symtab.update_new (name, fields) extfields) fieldext;
in Records_Data.put data thy end;
@@ -701,7 +698,8 @@
fun decode_type thy t =
let
- fun get_sort xs n = AList.lookup (op =) xs (n: indexname) |> the_default (Sign.defaultS thy);
+ fun get_sort env xi =
+ the_default (Sign.defaultS thy) (AList.lookup (op =) env (xi: indexname));
val map_sort = Sign.intern_sort thy;
in
Syntax.typ_of_term (get_sort (Syntax.term_sorts map_sort t)) map_sort t
@@ -711,6 +709,8 @@
(* parse translations *)
+local
+
fun gen_field_tr mark sfx (t as Const (c, _) $ Const (name, _) $ arg) =
if c = mark then Syntax.const (suffix sfx name) $ Abs ("_", dummyT, arg)
else raise TERM ("gen_field_tr: " ^ mark, [t])
@@ -721,17 +721,20 @@
else [gen_field_tr mark sfx tm]
| gen_fields_tr _ mark sfx tm = [gen_field_tr mark sfx tm];
+in
fun record_update_tr [t, u] =
fold (curry op $)
(gen_fields_tr @{syntax_const "_updates"} @{syntax_const "_update"} updateN u) t
| record_update_tr ts = raise TERM ("record_update_tr", ts);
-fun update_name_tr (Free (x, T) :: ts) = Free (suffix updateN x, T) $$ ts
- | update_name_tr (Const (x, T) :: ts) = Const (suffix updateN x, T) $$ ts
+end;
+
+fun update_name_tr (Free (x, T) :: ts) = list_comb (Free (suffix updateN x, T), ts)
+ | update_name_tr (Const (x, T) :: ts) = list_comb (Const (suffix updateN x, T), ts)
| update_name_tr (((c as Const (@{syntax_const "_constrain"}, _)) $ t $ ty) :: ts) =
(* FIXME @{type_syntax} *)
- (c $ update_name_tr [t] $ (Syntax.const "fun" $ ty $ Syntax.const "dummy")) $$ ts
+ list_comb (c $ update_name_tr [t] $ (Syntax.const "fun" $ ty $ Syntax.const "dummy"), ts)
| update_name_tr ts = raise TERM ("update_name_tr", ts);
fun dest_ext_field mark (t as (Const (c, _) $ Const (name, _) $ arg)) =
@@ -2091,15 +2094,18 @@
val upd_specs = map mk_upd_spec (fields_more ~~ lastN updator_thms);
(*derived operations*)
- val make_spec = Const (full (Binding.name makeN), all_types ---> recT0) $$ all_vars :==
- mk_rec (all_vars @ [HOLogic.unit]) 0;
- val fields_spec = Const (full (Binding.name fields_selN), types ---> Type extension) $$ vars :==
- mk_rec (all_vars @ [HOLogic.unit]) parent_len;
+ val make_spec =
+ list_comb (Const (full (Binding.name makeN), all_types ---> recT0), all_vars) :==
+ mk_rec (all_vars @ [HOLogic.unit]) 0;
+ val fields_spec =
+ list_comb (Const (full (Binding.name fields_selN), types ---> Type extension), vars) :==
+ mk_rec (all_vars @ [HOLogic.unit]) parent_len;
val extend_spec =
Const (full (Binding.name extendN), recT0 --> moreT --> rec_schemeT0) $ r_unit0 $ more :==
- mk_rec ((map (mk_sel r_unit0) all_fields) @ [more]) 0;
- val truncate_spec = Const (full (Binding.name truncateN), rec_schemeT0 --> recT0) $ r0 :==
- mk_rec ((map (mk_sel r0) all_fields) @ [HOLogic.unit]) 0;
+ mk_rec ((map (mk_sel r_unit0) all_fields) @ [more]) 0;
+ val truncate_spec =
+ Const (full (Binding.name truncateN), rec_schemeT0 --> recT0) $ r0 :==
+ mk_rec ((map (mk_sel r0) all_fields) @ [HOLogic.unit]) 0;
(* 2st stage: defs_thy *)