src/HOL/Tools/datatype_package.ML
changeset 22709 9ab51bac6287
parent 22675 acf10be7dcca
child 22777 2fc921376a86
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Sun Apr 15 23:25:49 2007 +0200
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Sun Apr 15 23:25:50 2007 +0200
     1.3 @@ -157,7 +157,7 @@
     1.4      val (types, sorts) = types_sorts state;
     1.5      fun types' (a, ~1) = (case AList.lookup (op =) params a of NONE => types(a, ~1) | sm => sm)
     1.6        | types' ixn = types ixn;
     1.7 -    val ([ct], _) = Thm.read_def_cterms (sign, types', sorts) [] false [(aterm, TypeInfer.logicT)];
     1.8 +    val ([ct], _) = Thm.read_def_cterms (sign, types', sorts) [] false [(aterm, dummyT)];
     1.9    in case #T (rep_cterm ct) of
    1.10         Type (tn, _) => tn
    1.11       | _ => error ("Cannot determine type of " ^ quote aterm)