--- a/src/HOL/Tools/numeral_syntax.ML Wed Mar 03 00:28:22 2010 +0100
+++ b/src/HOL/Tools/numeral_syntax.ML Wed Mar 03 00:32:14 2010 +0100
@@ -69,7 +69,7 @@
in
-fun numeral_tr' show_sorts (*"number_of"*) (Type (@{type_syntax fun}, [_, T])) (t :: ts) =
+fun numeral_tr' show_sorts (*"number_of"*) (Type (@{type_name fun}, [_, T])) (t :: ts) =
let val t' =
if not (! show_types) andalso can Term.dest_Type T then syntax_numeral t
else Syntax.const Syntax.constrainC $ syntax_numeral t $ Syntax.term_of_typ show_sorts T
--- a/src/HOL/Tools/record.ML Wed Mar 03 00:28:22 2010 +0100
+++ b/src/HOL/Tools/record.ML Wed Mar 03 00:32:14 2010 +0100
@@ -697,10 +697,8 @@
let
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
- |> Sign.intern_tycons thy
+ Syntax.typ_of_term (get_sort (Syntax.term_sorts t)) t
end;
@@ -752,8 +750,8 @@
val more' = mk_ext rest;
in
- (* FIXME authentic syntax *)
- list_comb (Syntax.const (suffix ext_typeN ext), alphas' @ [more'])
+ list_comb
+ (Syntax.const (Syntax.mark_type (suffix ext_typeN ext)), alphas' @ [more'])
end
| NONE => err ("no fields defined for " ^ ext))
| NONE => err (name ^ " is no proper field"))
@@ -857,7 +855,7 @@
val T = decode_type thy t;
val varifyT = varifyT (Term.maxidx_of_typ T);
- val term_of_type = Syntax.term_of_typ (! Syntax.show_sorts) o Sign.extern_typ thy;
+ val term_of_type = Syntax.term_of_typ (! Syntax.show_sorts);
fun strip_fields T =
(case T of
@@ -922,8 +920,7 @@
fun mk_type_abbr subst name alphas =
let val abbrT = Type (name, map (fn a => varifyT (TFree (a, Sign.defaultS thy))) alphas) in
- Syntax.term_of_typ (! Syntax.show_sorts)
- (Sign.extern_typ thy (Envir.norm_type subst abbrT))
+ Syntax.term_of_typ (! Syntax.show_sorts) (Envir.norm_type subst abbrT)
end;
fun match rT T = Sign.typ_match thy (varifyT rT, T) Vartab.empty;
@@ -946,14 +943,14 @@
fun record_ext_type_tr' name =
let
- val ext_type_name = suffix ext_typeN name;
+ val ext_type_name = Syntax.mark_type (suffix ext_typeN name);
fun tr' ctxt ts =
record_type_tr' ctxt (list_comb (Syntax.const ext_type_name, ts));
in (ext_type_name, tr') end;
fun record_ext_type_abbr_tr' abbr alphas zeta last_ext schemeT name =
let
- val ext_type_name = suffix ext_typeN name;
+ val ext_type_name = Syntax.mark_type (suffix ext_typeN name);
fun tr' ctxt ts =
record_type_abbr_tr' abbr alphas zeta last_ext schemeT ctxt
(list_comb (Syntax.const ext_type_name, ts));
@@ -1949,8 +1946,7 @@
val (args', more) = chop_last args;
fun mk_ext' ((name, T), args) more = mk_ext (name, T) (args @ [more]);
fun build Ts =
- fold_rev mk_ext' (drop n ((extension_names ~~ Ts) ~~ chunks parent_chunks args'))
- more;
+ fold_rev mk_ext' (drop n ((extension_names ~~ Ts) ~~ chunks parent_chunks args')) more;
in
if more = HOLogic.unit
then build (map_range recT (parent_len + 1))
@@ -1960,27 +1956,25 @@
val r_rec0 = mk_rec all_vars_more 0;
val r_rec_unit0 = mk_rec (all_vars @ [HOLogic.unit]) 0;
- fun r n = Free (rN, rec_schemeT n)
+ fun r n = Free (rN, rec_schemeT n);
val r0 = r 0;
- fun r_unit n = Free (rN, recT n)
+ fun r_unit n = Free (rN, recT n);
val r_unit0 = r_unit 0;
- val w = Free (wN, rec_schemeT 0)
+ val w = Free (wN, rec_schemeT 0);
(* print translations *)
- val external_names = Name_Space.external_names (Sign.naming_of ext_thy);
-
val record_ext_type_abbr_tr's =
let
- val trnames = external_names (hd extension_names);
+ val trname = hd extension_names;
val last_ext = unsuffix ext_typeN (fst extension);
- in map (record_ext_type_abbr_tr' name alphas zeta last_ext rec_schemeT0) trnames end;
+ in [record_ext_type_abbr_tr' name alphas zeta last_ext rec_schemeT0 trname] end;
val record_ext_type_tr's =
let
(*avoid conflict with record_type_abbr_tr's*)
- val trnames = if parent_len > 0 then external_names extension_name else [];
+ val trnames = if parent_len > 0 then [extension_name] else [];
in map record_ext_type_tr' trnames end;
val advanced_print_translation =
--- a/src/HOL/Tools/typedef.ML Wed Mar 03 00:28:22 2010 +0100
+++ b/src/HOL/Tools/typedef.ML Wed Mar 03 00:32:14 2010 +0100
@@ -118,7 +118,7 @@
fun add_def theory =
if def then
theory
- |> Sign.add_consts_i [(name, setT', NoSyn)] (* FIXME authentic syntax *)
+ |> Sign.add_consts_i [(name, setT', NoSyn)]
|> PureThy.add_defs false [((Thm.def_binding name, Logic.mk_equals (setC, set)), [])]
|-> (fn [th] => pair (SOME th))
else (NONE, theory);
--- a/src/HOL/Typerep.thy Wed Mar 03 00:28:22 2010 +0100
+++ b/src/HOL/Typerep.thy Wed Mar 03 00:32:14 2010 +0100
@@ -33,7 +33,7 @@
typed_print_translation {*
let
fun typerep_tr' show_sorts (*"typerep"*)
- (Type (@{type_syntax fun}, [Type (@{type_syntax itself}, [T]), _]))
+ (Type (@{type_name fun}, [Type (@{type_name itself}, [T]), _]))
(Const (@{const_syntax TYPE}, _) :: ts) =
Term.list_comb
(Syntax.const @{syntax_const "_TYPEREP"} $ Syntax.term_of_typ show_sorts T, ts)
--- a/src/HOL/ex/Numeral.thy Wed Mar 03 00:28:22 2010 +0100
+++ b/src/HOL/ex/Numeral.thy Wed Mar 03 00:32:14 2010 +0100
@@ -327,7 +327,7 @@
val k = int_of_num' n;
val t' = Syntax.const @{syntax_const "_Numerals"} $ Syntax.free ("#" ^ string_of_int k);
in case T
- of Type (@{type_syntax fun}, [_, T']) =>
+ of Type (@{type_name fun}, [_, T']) =>
if not (! show_types) andalso can Term.dest_Type T' then t'
else Syntax.const Syntax.constrainC $ t' $ Syntax.term_of_typ show_sorts T'
| T' => if T' = dummyT then t' else raise Match
--- a/src/Sequents/Sequents.thy Wed Mar 03 00:28:22 2010 +0100
+++ b/src/Sequents/Sequents.thy Wed Mar 03 00:32:14 2010 +0100
@@ -65,7 +65,7 @@
(* parse translation for sequences *)
-fun abs_seq' t = Abs ("s", Type (@{type_syntax seq'}, []), t);
+fun abs_seq' t = Abs ("s", Type (@{type_name seq'}, []), t);
fun seqobj_tr (Const (@{syntax_const "_SeqO"}, _) $ f) =
Const (@{const_syntax SeqO'}, dummyT) $ f