# HG changeset patch
# User wenzelm
# Date 1267572734 -3600
# Node ID df2862dc23a828d6d5773c2f93b3ffd7d044815a
# Parent  afa8cf9e63d84e0c08b2b48ddda8f92ce23aab23
adapted to authentic syntax -- actual types are verbatim;

diff -r afa8cf9e63d8 -r df2862dc23a8 src/HOL/Tools/numeral_syntax.ML
--- 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
diff -r afa8cf9e63d8 -r df2862dc23a8 src/HOL/Tools/record.ML
--- 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 =
diff -r afa8cf9e63d8 -r df2862dc23a8 src/HOL/Tools/typedef.ML
--- 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);
diff -r afa8cf9e63d8 -r df2862dc23a8 src/HOL/Typerep.thy
--- 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)
diff -r afa8cf9e63d8 -r df2862dc23a8 src/HOL/ex/Numeral.thy
--- 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
diff -r afa8cf9e63d8 -r df2862dc23a8 src/Sequents/Sequents.thy
--- 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