src/HOL/Tools/inductive_realizer.ML
changeset 56254 a2dd9200854d
parent 56245 84fc7dfa3cd4
child 58111 82db9ad610b9
     1.1 --- a/src/HOL/Tools/inductive_realizer.ML	Sat Mar 22 18:16:54 2014 +0100
     1.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Sat Mar 22 18:19:57 2014 +0100
     1.3 @@ -53,8 +53,8 @@
     1.4        | _ => vs)) (Term.add_vars prop []) [];
     1.5  
     1.6  val attach_typeS = map_types (map_atyps
     1.7 -  (fn TFree (s, []) => TFree (s, HOLogic.typeS)
     1.8 -    | TVar (ixn, []) => TVar (ixn, HOLogic.typeS)
     1.9 +  (fn TFree (s, []) => TFree (s, @{sort type})
    1.10 +    | TVar (ixn, []) => TVar (ixn, @{sort type})
    1.11      | T => T));
    1.12  
    1.13  fun dt_of_intrs thy vs nparms intrs =