src/HOL/ex/MT.thy
changeset 1026 f2dc38ed53ac
parent 972 e61b058d58d2
child 1151 c820b3cc3df0
--- a/src/HOL/ex/MT.thy	Mon Apr 10 08:47:43 1995 +0200
+++ b/src/HOL/ex/MT.thy	Mon Apr 10 08:49:00 1995 +0200
@@ -66,7 +66,7 @@
   ve_dom :: "ValEnv => ExVar set"
   ve_app :: "[ValEnv, ExVar] => Val"
 
-  clos_mk :: "[ExVar, Ex, ValEnv] => Clos" ("<| _  , _ , _ |>" [0,0,0] 1000)
+  clos_mk :: "[ExVar, Ex, ValEnv] => Clos" ("<| _ , _ , _ |>" [0,0,0] 1000)
 
   te_emp :: "TyEnv"
   te_owr :: "[TyEnv, ExVar, Ty] => TyEnv" ("_ + { _ |=> _ }" [36,0,0] 50)