# HG changeset patch
# User huffman
# Date 1269292273 25200
# Node ID 81608655c69ec0fa2e6abd7ed240d53e99700530
# Parent  12f09bf2c77fa2d89c83b1a897f2be74ffc16341
fix ML warnings in pcpodef.ML

diff -r 12f09bf2c77f -r 81608655c69e src/HOLCF/Tools/pcpodef.ML
--- a/src/HOLCF/Tools/pcpodef.ML	Mon Mar 22 13:27:35 2010 -0700
+++ b/src/HOLCF/Tools/pcpodef.ML	Mon Mar 22 14:11:13 2010 -0700
@@ -87,29 +87,32 @@
     val cpo_thms = map (Thm.transfer thy) [type_definition, below_def, admissible'];
     val (full_tname, Ts) = dest_Type newT;
     val lhs_sorts = map (snd o dest_TFree) Ts;
-    val thy2 =
-      thy
-      |> AxClass.prove_arity (full_tname, lhs_sorts, @{sort cpo})
-          (Tactic.rtac (@{thm typedef_cpo} OF cpo_thms) 1);
+    val tac = Tactic.rtac (@{thm typedef_cpo} OF cpo_thms) 1;
+    val thy = AxClass.prove_arity (full_tname, lhs_sorts, @{sort cpo}) tac thy;
     (* transfer thms so that they will know about the new cpo instance *)
-    val cpo_thms' = map (Thm.transfer thy2) cpo_thms;
+    val cpo_thms' = map (Thm.transfer thy) cpo_thms;
     fun make thm = Drule.export_without_context (thm OF cpo_thms');
-    val ([adm, cont_Rep, cont_Abs, lub, thelub, compact], thy3) =
-      thy2
+    val cont_Rep = make @{thm typedef_cont_Rep};
+    val cont_Abs = make @{thm typedef_cont_Abs};
+    val lub = make @{thm typedef_lub};
+    val thelub = make @{thm typedef_thelub};
+    val compact = make @{thm typedef_compact};
+    val (_, thy) =
+      thy
       |> Sign.add_path (Binding.name_of name)
       |> PureThy.add_thms
-        ([((Binding.prefix_name "adm_" name, admissible'), []),
-          ((Binding.prefix_name "cont_" Rep_name, make @{thm typedef_cont_Rep}), []),
-          ((Binding.prefix_name "cont_" Abs_name, make @{thm typedef_cont_Abs}), []),
-          ((Binding.prefix_name "lub_" name, make @{thm typedef_lub}), []),
-          ((Binding.prefix_name "thelub_" name, make @{thm typedef_thelub}), []),
-          ((Binding.prefix_name "compact_" name, make @{thm typedef_compact}), [])])
-      ||> Sign.restore_naming thy2;
+        ([((Binding.prefix_name "adm_"      name, admissible'), []),
+          ((Binding.prefix_name "cont_" Rep_name, cont_Rep   ), []),
+          ((Binding.prefix_name "cont_" Abs_name, cont_Abs   ), []),
+          ((Binding.prefix_name "lub_"      name, lub        ), []),
+          ((Binding.prefix_name "thelub_"   name, thelub     ), []),
+          ((Binding.prefix_name "compact_"  name, compact    ), [])])
+      ||> Sign.parent_path;
     val cpo_info : cpo_info =
       { below_def = below_def, adm = admissible', cont_Rep = cont_Rep,
         cont_Abs = cont_Abs, lub = lub, thelub = thelub, compact = compact };
   in
-    (cpo_info, thy3)
+    (cpo_info, thy)
   end;
 
 fun prove_pcpo
@@ -127,29 +130,33 @@
     val pcpo_thms = map (Thm.transfer thy) [type_definition, below_def, UU_mem'];
     val (full_tname, Ts) = dest_Type newT;
     val lhs_sorts = map (snd o dest_TFree) Ts;
-    val thy2 = thy
-      |> AxClass.prove_arity (full_tname, lhs_sorts, @{sort pcpo})
-        (Tactic.rtac (@{thm typedef_pcpo} OF pcpo_thms) 1);
-    val pcpo_thms' = map (Thm.transfer thy2) pcpo_thms;
+    val tac = Tactic.rtac (@{thm typedef_pcpo} OF pcpo_thms) 1;
+    val thy = AxClass.prove_arity (full_tname, lhs_sorts, @{sort pcpo}) tac thy;
+    val pcpo_thms' = map (Thm.transfer thy) pcpo_thms;
     fun make thm = Drule.export_without_context (thm OF pcpo_thms');
-    val ([Rep_strict, Abs_strict, Rep_strict_iff, Abs_strict_iff,
-          Rep_defined, Abs_defined], thy3) =
-      thy2
+    val Rep_strict = make @{thm typedef_Rep_strict};
+    val Abs_strict = make @{thm typedef_Abs_strict};
+    val Rep_strict_iff = make @{thm typedef_Rep_strict_iff};
+    val Abs_strict_iff = make @{thm typedef_Abs_strict_iff};
+    val Rep_defined = make @{thm typedef_Rep_defined};
+    val Abs_defined = make @{thm typedef_Abs_defined};
+    val (_, thy) =
+      thy
       |> Sign.add_path (Binding.name_of name)
       |> PureThy.add_thms
-        ([((Binding.suffix_name "_strict" Rep_name, make @{thm typedef_Rep_strict}), []),
-          ((Binding.suffix_name "_strict" Abs_name, make @{thm typedef_Abs_strict}), []),
-          ((Binding.suffix_name "_strict_iff" Rep_name, make @{thm typedef_Rep_strict_iff}), []),
-          ((Binding.suffix_name "_strict_iff" Abs_name, make @{thm typedef_Abs_strict_iff}), []),
-          ((Binding.suffix_name "_defined" Rep_name, make @{thm typedef_Rep_defined}), []),
-          ((Binding.suffix_name "_defined" Abs_name, make @{thm typedef_Abs_defined}), [])])
-      ||> Sign.restore_naming thy2;
+        ([((Binding.suffix_name "_strict"     Rep_name, Rep_strict), []),
+          ((Binding.suffix_name "_strict"     Abs_name, Abs_strict), []),
+          ((Binding.suffix_name "_strict_iff" Rep_name, Rep_strict_iff), []),
+          ((Binding.suffix_name "_strict_iff" Abs_name, Abs_strict_iff), []),
+          ((Binding.suffix_name "_defined"    Rep_name, Rep_defined), []),
+          ((Binding.suffix_name "_defined"    Abs_name, Abs_defined), [])])
+      ||> Sign.parent_path;
     val pcpo_info =
       { Rep_strict = Rep_strict, Abs_strict = Abs_strict,
         Rep_strict_iff = Rep_strict_iff, Abs_strict_iff = Abs_strict_iff,
         Rep_defined = Rep_defined, Abs_defined = Abs_defined };
   in
-    (pcpo_info, thy3)
+    (pcpo_info, thy)
   end;
 
 (* prepare_cpodef *)
@@ -319,7 +326,8 @@
     val args = map (apsnd (prep_constraint ctxt)) raw_args;
     val (goal1, goal2, make_result) =
       prepare_cpodef prep_term def name (b, args, mx) set opt_morphs thy;
-    fun after_qed [[th1, th2]] = ProofContext.theory (snd o make_result th1 th2);
+    fun after_qed [[th1, th2]] = ProofContext.theory (snd o make_result th1 th2)
+      | after_qed _ = error "cpodef_proof";
   in Proof.theorem_i NONE after_qed [[(goal1, []), (goal2, [])]] ctxt end;
 
 fun gen_pcpodef_proof prep_term prep_constraint
@@ -329,7 +337,8 @@
     val args = map (apsnd (prep_constraint ctxt)) raw_args;
     val (goal1, goal2, make_result) =
       prepare_pcpodef prep_term def name (b, args, mx) set opt_morphs thy;
-    fun after_qed [[th1, th2]] = ProofContext.theory (snd o make_result th1 th2);
+    fun after_qed [[th1, th2]] = ProofContext.theory (snd o make_result th1 th2)
+      | after_qed _ = error "pcpodef_proof";
   in Proof.theorem_i NONE after_qed [[(goal1, []), (goal2, [])]] ctxt end;
 
 in