src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy
changeset 42463 f270e3e18be5
parent 42187 b4f4ed5b8586
child 45125 c15b0faeb70a
--- a/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy	Fri Apr 22 15:57:43 2011 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy	Sat Apr 23 13:00:19 2011 +0200
@@ -110,7 +110,7 @@
   | TyAll type type  ("(3\<forall><:_./ _)" [0, 10] 10)
 
 datatype binding = VarB type | TVarB type
-types env = "binding list"
+type_synonym env = "binding list"
 
 primrec is_TVarB :: "binding \<Rightarrow> bool"
 where