src/HOL/Tools/typedef_package.ML
changeset 8100 6186ee807f2e
parent 7481 d44c77be268c
child 8141 d6d896e81cd7
     1.1 --- a/src/HOL/Tools/typedef_package.ML	Wed Jan 05 11:50:55 2000 +0100
     1.2 +++ b/src/HOL/Tools/typedef_package.ML	Wed Jan 05 11:56:04 2000 +0100
     1.3 @@ -89,7 +89,7 @@
     1.4  (* prepare_typedef *)
     1.5  
     1.6  fun read_term sg used s =
     1.7 -  #1 (Thm.read_def_cterm (sg, K None, K None) used true (s, HOLogic.termTVar));
     1.8 +  #1 (Thm.read_def_cterm (sg, K None, K None) used true (s, HOLogic.termT));
     1.9  
    1.10  fun cert_term sg _ t = Thm.cterm_of sg t handle TERM (msg, _) => error msg;
    1.11