src/Pure/Isar/object_logic.ML
changeset 14854 61bdf2ae4dc5
parent 14743 81001d6cb8c0
child 14981 e73f8140af78
     1.1 --- a/src/Pure/Isar/object_logic.ML	Tue Jun 01 11:25:26 2004 +0200
     1.2 +++ b/src/Pure/Isar/object_logic.ML	Tue Jun 01 12:33:50 2004 +0200
     1.3 @@ -115,7 +115,7 @@
     1.4  fun fixed_judgment sg x =
     1.5    let  (*be robust wrt. low-level errors*)
     1.6      val c = judgment_name sg;
     1.7 -    val aT = TFree ("'a", logicS);
     1.8 +    val aT = TFree ("'a", []);
     1.9      val T =
    1.10        if_none (Sign.const_type sg c) (aT --> propT)
    1.11        |> Term.map_type_tvar (fn ((x, _), S) => TFree (x, S));