# HG changeset patch
# User clasohm
# Date 817819414 -3600
# Node ID 57777949b2f8895411ac11244ae0d00f95cb7d0f
# Parent  2f8055af9c0492067670a1fff2669715c4464ebc
removed some more quotes

diff -r 2f8055af9c04 -r 57777949b2f8 src/HOL/Subst/UTLemmas.thy
--- a/src/HOL/Subst/UTLemmas.thy	Fri Dec 01 12:27:09 1995 +0100
+++ b/src/HOL/Subst/UTLemmas.thy	Fri Dec 01 13:03:34 1995 +0100
@@ -9,8 +9,8 @@
 
 consts
 
-  vars_of       ::   "'a uterm=>'a set"
-  "<:"          ::   "['a uterm,'a uterm]=>bool"   (infixl 54) 
+  vars_of       ::   'a uterm=>'a set
+  "<:"          ::   ['a uterm,'a uterm]=>bool   (infixl 54) 
 
 rules  (*Definitions*)
 
diff -r 2f8055af9c04 -r 57777949b2f8 src/HOL/Subst/UTerm.thy
--- a/src/HOL/Subst/UTerm.thy	Fri Dec 01 12:27:09 1995 +0100
+++ b/src/HOL/Subst/UTerm.thy	Fri Dec 01 13:03:34 1995 +0100
@@ -23,10 +23,10 @@
   Var       :: 'a => 'a uterm
   Const     :: 'a => 'a uterm
   Comb      :: ['a uterm, 'a uterm] => 'a uterm
-  UTerm_rec :: "['a item, 'a item => 'b, 'a item => 'b, 
-                ['a item , 'a item, 'b, 'b]=>'b] => 'b"
-  uterm_rec :: "['a uterm, 'a => 'b, 'a => 'b, 
-                ['a uterm, 'a uterm,'b,'b]=>'b] => 'b"
+  UTerm_rec :: ['a item, 'a item => 'b, 'a item => 'b, 
+                ['a item , 'a item, 'b, 'b]=>'b] => 'b
+  uterm_rec :: ['a uterm, 'a => 'b, 'a => 'b, 
+                ['a uterm, 'a uterm,'b,'b]=>'b] => 'b
 
 defs
      (*defining the concrete constructors*)
diff -r 2f8055af9c04 -r 57777949b2f8 src/HOL/ex/Simult.thy
--- a/src/HOL/ex/Simult.thy	Fri Dec 01 12:27:09 1995 +0100
+++ b/src/HOL/ex/Simult.thy	Fri Dec 01 13:03:34 1995 +0100
@@ -31,12 +31,12 @@
   Tcons       :: ['a, 'a forest] => 'a tree
   Fcons       :: ['a tree, 'a forest] => 'a forest
   Fnil        :: 'a forest
-  TF_rec      :: "['a item, ['a item , 'a item, 'b]=>'b,     
-                 'b, ['a item , 'a item, 'b, 'b]=>'b] => 'b"
-  tree_rec    :: "['a tree, ['a, 'a forest, 'b]=>'b,          
-                 'b, ['a tree, 'a forest, 'b, 'b]=>'b] => 'b"
-  forest_rec  :: "['a forest, ['a, 'a forest, 'b]=>'b,        
-                  'b, ['a tree, 'a forest, 'b, 'b]=>'b] => 'b"
+  TF_rec      :: ['a item, ['a item , 'a item, 'b]=>'b,     
+                 'b, ['a item , 'a item, 'b, 'b]=>'b] => 'b
+  tree_rec    :: ['a tree, ['a, 'a forest, 'b]=>'b,          
+                 'b, ['a tree, 'a forest, 'b, 'b]=>'b] => 'b
+  forest_rec  :: ['a forest, ['a, 'a forest, 'b]=>'b,        
+                  'b, ['a tree, 'a forest, 'b, 'b]=>'b] => 'b
 
 defs
      (*the concrete constants*)