src/HOL/Tools/Function/fundef_datatype.ML

--- a/src/HOL/Tools/Function/fundef_datatype.ML	Fri Sep 25 10:20:03 2009 +0200
+++ b/src/HOL/Tools/Function/fundef_datatype.ML	Sun Sep 27 09:52:23 2009 +0200
@@ -145,7 +145,7 @@
          let
              val T = fastype_of v
              val (tname, _) = dest_Type T
-             val {exhaustion=case_thm, ...} = Datatype.the_info thy tname
+             val {exhaust=case_thm, ...} = Datatype.the_info thy tname
              val constrs = inst_constrs_of thy T
              val c_cases = map (constr_case thy P idx (v :: vs) pts) constrs
          in