Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
merged
authorwenzelm
Sat, 11 May 2013 22:20:59 +0200
changeset 51936 972c4f42fd52
parent 51928 a5265222d6e6 (diff)
parent 51935 916c7fe684e3 (current diff)
child 51937 db22d73e6c3e
merged
lib/ProofGeneral/README file | annotate | diff | comparison | revisions
lib/ProofGeneral/pgip.rnc file | annotate | diff | comparison | revisions
lib/ProofGeneral/pgip_isar.xml file | annotate | diff | comparison | revisions
lib/ProofGeneral/pgml.rnc file | annotate | diff | comparison | revisions
lib/ProofGeneral/schemas.xml file | annotate | diff | comparison | revisions
lib/Tools/mkproject file | annotate | diff | comparison | revisions
src/Pure/ProofGeneral/TODO file | annotate | diff | comparison | revisions
src/Pure/ProofGeneral/pgip.ML file | annotate | diff | comparison | revisions
src/Pure/ProofGeneral/pgip_tests.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Sat May 11 22:17:18 2013 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Sat May 11 22:20:59 2013 +0200
@@ -1379,9 +1379,11 @@
       in
         case min_R of
           Vect (k, Atom _) => kk_vect_set_bool_op connective k r1 r2
-        | Func (_, Formula Neut) => set_oper r1 r2
-        | Func (_, Atom _) => set_oper (kk_join r1 true_atom)
-                                       (kk_join r2 true_atom)
+        | Func (_, R') =>
+          (case body_rep R' of
+             Formula Neut => set_oper r1 r2
+           | Atom _ => set_oper (kk_join r1 true_atom) (kk_join r2 true_atom)
+           | _ => raise REP ("Nitpick_Kodkod.to_set_bool_op", [min_R]))
         | _ => raise REP ("Nitpick_Kodkod.to_set_bool_op", [min_R])
       end
     and to_bit_word_unary_op T R oper =
isabelle