# HG changeset patch
# User nipkow
# Date 813406955 -3600
# Node ID f59b4f9f2cdc50d4092de893a75d9a53b5989fa4
# Parent  7e6189fc833c0970991769b984512aeecef68f4c
All constants introduced by datatype now operate on class term explicitly.
They used to take the default class.

diff -r 7e6189fc833c -r f59b4f9f2cdc src/HOL/datatype.ML
--- a/src/HOL/datatype.ML	Wed Oct 11 10:09:56 1995 +0100
+++ b/src/HOL/datatype.ML	Wed Oct 11 11:22:35 1995 +0100
@@ -193,7 +193,7 @@
 
      (*Pretty printers for type lists;
        pp_typlist1: parentheses, pp_typlist2: brackets*)
-      fun pp_typ (dtVar s) = s
+      fun pp_typ (dtVar s) = "(" ^ s ^ "::term)"
         | pp_typ (dtTyp (typvars, id)) =
 	  if null typvars then id else (pp_typlist1 typvars) ^ id
         | pp_typ (dtRek (typvars, id)) = (pp_typlist1 typvars) ^ id
@@ -294,7 +294,7 @@
       val case_const =
 	(t_case,
 	 "[" ^ gen_typlist new_tvar_name I cons_list 
-	 ^  pp_typlist1 typevars ^ tname ^ "] =>" ^ new_tvar_name,
+	 ^  pp_typlist1 typevars ^ tname ^ "] =>" ^ new_tvar_name^"::term",
 	 NoSyn);
 
       val rules_case = case_rules 1 cons_list;
@@ -330,7 +330,7 @@
       val rec_const =
 	(t_rec,
 	 "[" ^ (gen_typlist new_tvar_name add_reks cons_list) 
-	 ^ (pp_typlist1 typevars) ^ tname ^ "] =>" ^ new_tvar_name,
+	 ^ (pp_typlist1 typevars) ^ tname ^ "] =>" ^ new_tvar_name^"::term",
 	 NoSyn);
 
       val rules_rec = rec_rules 1 cons_list