# HG changeset patch
# User wenzelm
# Date 1330609712 -3600
# Node ID b91628b2522b69607a453f5973eb88cedc8dd899
# Parent  a10dcc985e8d70232817a2c7487f36069ad45ecc# Parent  125e49d04cf6cccdf615f474b4a7102d90901989
merged

diff -r 125e49d04cf6 -r b91628b2522b src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu Mar 01 14:48:28 2012 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu Mar 01 14:48:32 2012 +0100
@@ -744,10 +744,11 @@
     try (Quotient_Term.absrep_const_chk ctxt Quotient_Term.AbsF) s'
     = SOME (Const x) andalso not (is_codatatype ctxt abs_T)
   | is_quot_abs_fun _ _ = false
-fun is_quot_rep_fun ctxt (x as (_, Type (@{type_name fun},
-                                         [abs_T as Type (s', _), _]))) =
-    try (Quotient_Term.absrep_const_chk ctxt Quotient_Term.RepF) s'
-    = SOME (Const x) andalso not (is_codatatype ctxt abs_T)
+fun is_quot_rep_fun ctxt (x as (s, Type (@{type_name fun},
+                                         [abs_T as Type (abs_s, _), _]))) =
+    (case try (Quotient_Term.absrep_const_chk ctxt Quotient_Term.RepF) abs_s of
+       SOME (Const (s', _)) => s = s' andalso not (is_codatatype ctxt abs_T)
+     | NONE => false)
   | is_quot_rep_fun _ _ = false
 
 fun mate_of_rep_fun ctxt (x as (_, Type (@{type_name fun},
@@ -767,7 +768,8 @@
     raise TYPE ("Nitpick_HOL.rep_type_for_quot_type", [T], [])
 fun equiv_relation_for_quot_type thy (Type (s, Ts)) =
     let
-      val {qtyp, equiv_rel, equiv_thm, ...} = the (Quotient_Info.lookup_quotients thy s)
+      val {qtyp, equiv_rel, equiv_thm, ...} =
+        the (Quotient_Info.lookup_quotients thy s)
       val partial =
         case prop_of equiv_thm of
           @{const Trueprop} $ (Const (@{const_name equivp}, _) $ _) => false
@@ -1785,12 +1787,14 @@
                   else if is_quot_type ctxt (domain_type T) then
                     let
                       val abs_T = domain_type T
-                      val rep_T = domain_type (range_type T)
+                      val rep_T = elem_type (range_type T)
                       val (rep_fun, _) = quot_rep_of depth Ts abs_T rep_T []
                       val (equiv_rel, _) =
                         equiv_relation_for_quot_type ctxt abs_T
                     in
-                      (Abs (Name.uu, abs_T, equiv_rel $ (rep_fun $ Bound 0)),
+                      (Abs (Name.uu, abs_T,
+                            HOLogic.Collect_const rep_T
+                            $ (equiv_rel $ (rep_fun $ Bound 0))),
                        ts)
                     end
                   else
diff -r 125e49d04cf6 -r b91628b2522b src/HOL/Tools/Nitpick/nitpick_kodkod.ML
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Thu Mar 01 14:48:28 2012 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Thu Mar 01 14:48:32 2012 +0100
@@ -1060,7 +1060,7 @@
       | Op1 (Finite, _, Opt (Atom _), _) => KK.None
       | Op1 (Converse, T, R, u1) =>
         let
-          val (b_T, a_T) = HOLogic.dest_prodT (elem_type T)
+          val (b_T, a_T) = HOLogic.dest_prodT (pseudo_domain_type T)
           val (b_R, a_R) =
             case R of
               Func (Struct [R1, R2], _) => (R1, R2)
@@ -1191,8 +1191,8 @@
         end
       | Op2 (Composition, _, R, u1, u2) =>
         let
-          val (a_T, b_T) = HOLogic.dest_prodT (elem_type (type_of u1))
-          val (_, c_T) = HOLogic.dest_prodT (elem_type (type_of u2))
+          val (a_T, b_T) = HOLogic.dest_prodT (pseudo_domain_type (type_of u1))
+          val (_, c_T) = HOLogic.dest_prodT (pseudo_domain_type (type_of u2))
           val ab_k = card_of_domain_from_rep 2 (rep_of u1)
           val bc_k = card_of_domain_from_rep 2 (rep_of u2)
           val ac_k = card_of_domain_from_rep 2 R
diff -r 125e49d04cf6 -r b91628b2522b src/HOL/Tools/SMT/smt_solver.ML
--- a/src/HOL/Tools/SMT/smt_solver.ML	Thu Mar 01 14:48:28 2012 +0100
+++ b/src/HOL/Tools/SMT/smt_solver.ML	Thu Mar 01 14:48:32 2012 +0100
@@ -65,7 +65,9 @@
 fun run ctxt name mk_cmd input =
   (case SMT_Config.certificates_of ctxt of
     NONE =>
-      if Config.get ctxt SMT_Config.debug_files = "" then
+      if not (SMT_Config.is_available ctxt name) then
+        error ("The SMT solver " ^ quote name ^ " is not installed.")
+      else if Config.get ctxt SMT_Config.debug_files = "" then
         trace_and ctxt ("Invoking SMT solver " ^ quote name ^ " ...")
           (Cache_IO.run mk_cmd) input
       else
@@ -237,13 +239,10 @@
 fun gen_apply (ithms, ctxt) =
   let val (name, {command, reconstruct, ...}) = name_and_info_of ctxt
   in
-    if not (SMT_Config.is_available ctxt name) then
-      error ("The SMT solver " ^ quote name ^ " is not installed.")
-    else
-      (ithms, ctxt)
-      |-> invoke name command
-      |> reconstruct ctxt
-      |>> distinct (op =)
+    (ithms, ctxt)
+    |-> invoke name command
+    |> reconstruct ctxt
+    |>> distinct (op =)
   end
 
 fun apply_solver ctxt = gen_apply o gen_preprocess ctxt