# HG changeset patch
# User wenzelm
# Date 1193429442 -7200
# Node ID 5b5659801257a17e93f233f8bf5c3900d404790e
# Parent  bc21d8de18a917ddf1816fa3365ca8f9a098e251
export class_prefix;
removed obsolete const hiding;

diff -r bc21d8de18a9 -r 5b5659801257 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Fri Oct 26 21:22:20 2007 +0200
+++ b/src/Pure/Isar/class.ML	Fri Oct 26 22:10:42 2007 +0200
@@ -29,6 +29,7 @@
   val prove_subclass: class * class -> thm list -> Proof.context
     -> theory -> theory
   val print_classes: theory -> unit
+  val class_prefix: string -> string
   val uncheck: bool ref
 
   val instance_arity: (theory -> theory) -> arity list -> theory -> Proof.state
@@ -870,11 +871,8 @@
     val ty' = Term.fastype_of dict';
     val ty'' = Type.strip_sorts ty';
     val def_eq = Logic.mk_equals (Const (c', ty'), dict');
-
-    val c'' = NameSpace.full (Sign.naming_of thy' |> NameSpace.add_path prfx) c;
   in
     thy'
-    |> Sign.hide_consts_i false [c''] (*FIXME*)
     |> Sign.declare_const pos (c, ty'', mx) |> snd
     |> Thm.add_def false (c, def_eq)
     |>> Thm.symmetric
@@ -897,13 +895,8 @@
     val rews = map (Logic.dest_equals o Thm.prop_of) (these_defs thy' [class])
     val rhs' = (Pattern.rewrite_term thy rews [] o Morphism.term phi) rhs;
     val ty' = (Logic.unvarifyT o Term.fastype_of) rhs';
-
-    val c'' = NameSpace.full (Sign.naming_of thy' |> NameSpace.add_path prfx) c;
-    val ty'' = (Type.strip_sorts o Logic.unvarifyT) (Sign.the_const_constraint thy' c'');
   in
     thy'
-    |> Sign.add_const_constraint (c'', SOME ty'') (*FIXME*)
-    |> Sign.hide_consts_i false [c''] (*FIXME*)
     |> Sign.add_abbrev (#1 prmode) pos (c, map_types Type.strip_sorts rhs') |> snd
     |> Sign.add_const_constraint (c', SOME ty')
     |> Sign.notation true prmode [(Const (c', ty'), mx)]