Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/inductive_realizer.ML
changeset 47060 e2741ec9ae36
parent 46708 b138dee7bed3
child 49170 03bee3a6a1b7 
--- a/src/HOL/Tools/inductive_realizer.ML	Tue Mar 20 21:37:31 2012 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML	Wed Mar 21 11:00:34 2012 +0100
@@ -505,7 +505,7 @@
       (case HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of thm)) of
            [_] => [pred_of (HOLogic.dest_Trueprop (hd (prems_of thm)))]
          | xs => map (pred_of o fst o HOLogic.dest_imp) xs)
-         handle TERM _ => err () | Empty => err ();
+         handle TERM _ => err () | List.Empty => err ();
   in 
     add_ind_realizers (hd sets)
       (case arg of
isabelle