src/Pure/Isar/class.ML
changeset 25210 5b5659801257
parent 25209 bc21d8de18a9
child 25239 3d6abdd10382
     1.1 --- a/src/Pure/Isar/class.ML	Fri Oct 26 21:22:20 2007 +0200
     1.2 +++ b/src/Pure/Isar/class.ML	Fri Oct 26 22:10:42 2007 +0200
     1.3 @@ -29,6 +29,7 @@
     1.4    val prove_subclass: class * class -> thm list -> Proof.context
     1.5      -> theory -> theory
     1.6    val print_classes: theory -> unit
     1.7 +  val class_prefix: string -> string
     1.8    val uncheck: bool ref
     1.9  
    1.10    val instance_arity: (theory -> theory) -> arity list -> theory -> Proof.state
    1.11 @@ -870,11 +871,8 @@
    1.12      val ty' = Term.fastype_of dict';
    1.13      val ty'' = Type.strip_sorts ty';
    1.14      val def_eq = Logic.mk_equals (Const (c', ty'), dict');
    1.15 -
    1.16 -    val c'' = NameSpace.full (Sign.naming_of thy' |> NameSpace.add_path prfx) c;
    1.17    in
    1.18      thy'
    1.19 -    |> Sign.hide_consts_i false [c''] (*FIXME*)
    1.20      |> Sign.declare_const pos (c, ty'', mx) |> snd
    1.21      |> Thm.add_def false (c, def_eq)
    1.22      |>> Thm.symmetric
    1.23 @@ -897,13 +895,8 @@
    1.24      val rews = map (Logic.dest_equals o Thm.prop_of) (these_defs thy' [class])
    1.25      val rhs' = (Pattern.rewrite_term thy rews [] o Morphism.term phi) rhs;
    1.26      val ty' = (Logic.unvarifyT o Term.fastype_of) rhs';
    1.27 -
    1.28 -    val c'' = NameSpace.full (Sign.naming_of thy' |> NameSpace.add_path prfx) c;
    1.29 -    val ty'' = (Type.strip_sorts o Logic.unvarifyT) (Sign.the_const_constraint thy' c'');
    1.30    in
    1.31      thy'
    1.32 -    |> Sign.add_const_constraint (c'', SOME ty'') (*FIXME*)
    1.33 -    |> Sign.hide_consts_i false [c''] (*FIXME*)
    1.34      |> Sign.add_abbrev (#1 prmode) pos (c, map_types Type.strip_sorts rhs') |> snd
    1.35      |> Sign.add_const_constraint (c', SOME ty')
    1.36      |> Sign.notation true prmode [(Const (c', ty'), mx)]