src/LCF/simpdata.ML
changeset 65 08d3c007ae7c
parent 0 a5a9c433f639
child 190 4ae10fc91cba
     1.1 --- a/src/LCF/simpdata.ML	Thu Oct 21 14:56:12 1993 +0100
     1.2 +++ b/src/LCF/simpdata.ML	Thu Oct 21 14:59:54 1993 +0100
     1.3 @@ -1,7 +1,7 @@
     1.4  (*  Title: 	LCF/simpdata
     1.5      ID:         $Id$
     1.6      Author: 	Tobias Nipkow, Cambridge University Computer Laboratory
     1.7 -    Copyright   1991  University of Cambridge
     1.8 +    Copyright   1993  University of Cambridge
     1.9  
    1.10  Simplification data for LCF
    1.11  *)
    1.12 @@ -10,7 +10,7 @@
    1.13  fun mk_rew_rules r =
    1.14  let fun basify thm =
    1.15  	  (case concl_of thm of
    1.16 -             _$(_$t$_) => (case fastype_of([],t) of
    1.17 +             _$(_$t$_) => (case fastype_of t of
    1.18  	                     Type("fun",_) => basify(thm RS ap_thm)
    1.19  	                   | _ => thm)
    1.20             | _ => thm)