src/Pure/sign.ML
changeset 19391 4812d28c90a6
parent 19384 c5ee8f756683
child 19407 7c7a2e337504
--- a/src/Pure/sign.ML	Sun Apr 09 19:41:30 2006 +0200
+++ b/src/Pure/sign.ML	Mon Apr 10 00:33:49 2006 +0200
@@ -813,7 +813,7 @@
       val syn' = Syntax.extend_consts [bclass] syn;
       val tsig' = Type.add_classes (pp thy) naming [(bclass, classes)] tsig;
     in (naming, syn', tsig', consts) end)
-  |> add_consts_i [(Logic.const_of_class bclass, a_itselfT --> propT, NoSyn)];
+  |> add_consts_i [(Logic.const_of_class bclass, Term.a_itselfT --> propT, NoSyn)];
 
 val add_classes = fold (gen_add_class intern_class);
 val add_classes_i = fold (gen_add_class (K I));