src/HOL/Subst/UTerm.thy
changeset 1381 57777949b2f8
parent 1374 5e407f2a3323
child 1476 608483c2122a
     1.1 --- a/src/HOL/Subst/UTerm.thy	Fri Dec 01 12:27:09 1995 +0100
     1.2 +++ b/src/HOL/Subst/UTerm.thy	Fri Dec 01 13:03:34 1995 +0100
     1.3 @@ -23,10 +23,10 @@
     1.4    Var       :: 'a => 'a uterm
     1.5    Const     :: 'a => 'a uterm
     1.6    Comb      :: ['a uterm, 'a uterm] => 'a uterm
     1.7 -  UTerm_rec :: "['a item, 'a item => 'b, 'a item => 'b, 
     1.8 -                ['a item , 'a item, 'b, 'b]=>'b] => 'b"
     1.9 -  uterm_rec :: "['a uterm, 'a => 'b, 'a => 'b, 
    1.10 -                ['a uterm, 'a uterm,'b,'b]=>'b] => 'b"
    1.11 +  UTerm_rec :: ['a item, 'a item => 'b, 'a item => 'b, 
    1.12 +                ['a item , 'a item, 'b, 'b]=>'b] => 'b
    1.13 +  uterm_rec :: ['a uterm, 'a => 'b, 'a => 'b, 
    1.14 +                ['a uterm, 'a uterm,'b,'b]=>'b] => 'b
    1.15  
    1.16  defs
    1.17       (*defining the concrete constructors*)