src/HOL/Tools/Function/pat_completeness.ML
changeset 47060 e2741ec9ae36
parent 42361 23f352990944
child 47432 e1576d13e933
     1.1 --- a/src/HOL/Tools/Function/pat_completeness.ML	Tue Mar 20 21:37:31 2012 +0100
     1.2 +++ b/src/HOL/Tools/Function/pat_completeness.ML	Wed Mar 21 11:00:34 2012 +0100
     1.3 @@ -143,7 +143,7 @@
     1.4  
     1.5      val (qss, x_pats) = split_list (map pat_of cases)
     1.6      val xs = map fst (hd x_pats)
     1.7 -      handle Empty => raise COMPLETENESS
     1.8 +      handle List.Empty => raise COMPLETENESS
     1.9  
    1.10      val patss = map (map snd) x_pats
    1.11      val complete_thm = prove_completeness thy xs thesis qss patss