--- a/src/HOL/Typedef.thy Tue Feb 03 19:48:06 2009 +0100
+++ b/src/HOL/Typedef.thy Tue Feb 03 21:26:21 2009 +0100
@@ -119,52 +119,4 @@
use "Tools/typecopy_package.ML" setup TypecopyPackage.setup
use "Tools/typedef_codegen.ML" setup TypedefCodegen.setup
-
-text {* This class is just a workaround for classes without parameters;
- it shall disappear as soon as possible. *}
-
-class itself =
- fixes itself :: "'a itself"
-
-setup {*
-let fun add_itself tyco thy =
- let
- val vs = Name.names Name.context "'a"
- (replicate (Sign.arity_number thy tyco) @{sort type});
- val ty = Type (tyco, map TFree vs);
- val lhs = Const (@{const_name itself}, Term.itselfT ty);
- val rhs = Logic.mk_type ty;
- val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
- in
- thy
- |> TheoryTarget.instantiation ([tyco], vs, @{sort itself})
- |> `(fn lthy => Syntax.check_term lthy eq)
- |-> (fn eq => Specification.definition (NONE, (Attrib.empty_binding, eq)))
- |> snd
- |> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
- |> LocalTheory.exit_global
- end
-in TypedefPackage.interpretation add_itself end
-*}
-
-instantiation bool :: itself
-begin
-
-definition "itself = TYPE(bool)"
-
-instance ..
-
end
-
-instantiation "fun" :: ("type", "type") itself
-begin
-
-definition "itself = TYPE('a \<Rightarrow> 'b)"
-
-instance ..
-
-end
-
-hide (open) const itself
-
-end