# HG changeset patch
# User haftmann
# Date 1220350054 -7200
# Node ID 5e9f00f4f209ab8897b094bf053b1629323bf457
# Parent  a45e8c872dc19848a29f7988b52db8340af5c64a
adapted to class instantiation compliance

diff -r a45e8c872dc1 -r 5e9f00f4f209 src/HOLCF/Pcpodef.thy
--- a/src/HOLCF/Pcpodef.thy	Mon Sep 01 22:10:42 2008 +0200
+++ b/src/HOLCF/Pcpodef.thy	Tue Sep 02 12:07:34 2008 +0200
@@ -17,8 +17,10 @@
   if the ordering is defined in the standard way.
 *}
 
+setup {* Sign.add_const_constraint (@{const_name Porder.sq_le}, NONE) *}
+
 theorem typedef_po:
-  fixes Abs :: "'a::po \<Rightarrow> 'b::sq_ord"
+  fixes Abs :: "'a::po \<Rightarrow> 'b::type"
   assumes type: "type_definition Rep Abs A"
     and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
   shows "OFCLASS('b, po_class)"
@@ -29,6 +31,9 @@
  apply (erule (1) antisym_less)
 done
 
+setup {* Sign.add_const_constraint (@{const_name Porder.sq_le},
+  SOME @{typ "'a::sq_ord \<Rightarrow> 'a::sq_ord \<Rightarrow> bool"}) *}
+
 subsection {* Proving a subtype is finite *}
 
 lemma typedef_finite_UNIV:
diff -r a45e8c872dc1 -r 5e9f00f4f209 src/HOLCF/Tools/pcpodef_package.ML
--- a/src/HOLCF/Tools/pcpodef_package.ML	Mon Sep 01 22:10:42 2008 +0200
+++ b/src/HOLCF/Tools/pcpodef_package.ML	Tue Sep 02 12:07:34 2008 +0200
@@ -83,18 +83,26 @@
     val (Rep_name, Abs_name) = the_default ("Rep_" ^ name, "Abs_" ^ name) opt_morphs;
     val RepC = Const (full Rep_name, newT --> oldT);
     fun lessC T = Const (@{const_name Porder.sq_le}, T --> T --> HOLogic.boolT);
-    val less_def = ("less_" ^ name ^ "_def", Logic.mk_equals (lessC newT,
-      Abs ("x", newT, Abs ("y", newT, lessC oldT $ (RepC $ Bound 1) $ (RepC $ Bound 0)))));
+    val less_def = Logic.mk_equals (lessC newT,
+      Abs ("x", newT, Abs ("y", newT, lessC oldT $ (RepC $ Bound 1) $ (RepC $ Bound 0))));
 
-    fun make_po tac theory = theory
-      |> TypedefPackage.add_typedef_i def (SOME name) (t, vs, mx) set opt_morphs tac
-      ||> AxClass.prove_arity (full_tname, lhs_sorts, ["Porder.sq_ord"])
-           (Class.intro_classes_tac [])
-      ||>> PureThy.add_defs true [Thm.no_attributes less_def]
-      |-> (fn ((_, {type_definition, set_def, ...}), [less_definition]) =>
-          AxClass.prove_arity (full_tname, lhs_sorts, ["Porder.po"])
-             (Tactic.rtac (typedef_po OF [type_definition, less_definition]) 1)
-           #> pair (type_definition, less_definition, set_def));
+    fun make_po tac thy1 =
+      let
+        val ((_, {type_definition, set_def, ...}), thy2) = thy1
+          |> TypedefPackage.add_typedef_i def (SOME name) (t, vs, mx) set opt_morphs tac;
+        val lthy3 = thy2
+          |> TheoryTarget.instantiation ([full_tname], lhs_tfrees, @{sort "Porder.po"});
+        val less_def' = Syntax.check_term lthy3 less_def;
+        val ((_, (_, less_definition')), lthy4) = lthy3
+          |> Specification.definition (NONE, (("less_" ^ name ^ "_def", []), less_def'));
+        val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy4);
+        val less_definition = singleton (ProofContext.export lthy4 ctxt_thy) less_definition';
+        val thy5 = lthy4
+          |> Class.prove_instantiation_instance
+              (K (Tactic.rtac (typedef_po OF [type_definition, less_definition]) 1))
+          |> LocalTheory.exit
+          |> ProofContext.theory_of;
+      in ((type_definition, less_definition, set_def), thy5) end;
 
     fun make_cpo admissible (type_def, less_def, set_def) theory =
       let