# HG changeset patch
# User lcp
# Date 797161782 -7200
# Node ID 0f9230a24164b001f8be561ab2f2c580c2ce0ee9
# Parent  63e249badea6ff35204ab6972f234627bff61003
Deleted extra space in clos_mk.

diff -r 63e249badea6 -r 0f9230a24164 ex/MT.thy
--- a/ex/MT.thy	Thu Apr 06 11:47:00 1995 +0200
+++ b/ex/MT.thy	Thu Apr 06 11:49:42 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)