src/Pure/Isar/object_logic.ML

--- a/src/Pure/Isar/object_logic.ML	Tue Jun 01 11:25:26 2004 +0200
+++ b/src/Pure/Isar/object_logic.ML	Tue Jun 01 12:33:50 2004 +0200
@@ -115,7 +115,7 @@
 fun fixed_judgment sg x =
   let  (*be robust wrt. low-level errors*)
     val c = judgment_name sg;
-    val aT = TFree ("'a", logicS);
+    val aT = TFree ("'a", []);
     val T =
       if_none (Sign.const_type sg c) (aT --> propT)
       |> Term.map_type_tvar (fn ((x, _), S) => TFree (x, S));