src/Pure/axclass.ML
changeset 18932 66ecb05f92c8
parent 18848 4ed69fe8f887
child 18964 67f572e03236
--- a/src/Pure/axclass.ML	Mon Feb 06 20:58:57 2006 +0100
+++ b/src/Pure/axclass.ML	Mon Feb 06 20:58:59 2006 +0100
@@ -200,7 +200,7 @@
     (*declare axioms and rule*)
     val (([intro], [axioms]), axms_thy) =
       class_thy
-      |> Theory.add_path (Sign.const_of_class bclass)
+      |> Theory.add_path (Logic.const_of_class bclass)
       |> PureThy.add_axioms_i [Thm.no_attributes (introN, intro_axm)]
       ||>> PureThy.add_axiomss_i [Thm.no_attributes (axiomsN, abs_axms)];
     val info = {super_classes = super_classes, intro = intro, axioms = axioms};
@@ -208,7 +208,7 @@
     (*store info*)
     val (_, final_thy) =
       axms_thy
-      |> Theory.add_finals_i false [Const (Sign.const_of_class class, a_itselfT --> propT)]
+      |> Theory.add_finals_i false [Const (Logic.const_of_class class, a_itselfT --> propT)]
       |> PureThy.add_thms ((map #1 axms ~~ axioms) ~~ atts)
       ||> Theory.restore_naming class_thy
       ||> AxclassesData.map (Symtab.update (class, info));