# HG changeset patch
# User bulwahn
# Date 1290418923 -3600
# Node ID 5615cc557120500e6d81d609ec0e905249006df9
# Parent  3fa1c2472568721a3bd2ce50074699dc8103e457
moving the error handling to the right scope in smallvalue_generators

diff -r 3fa1c2472568 -r 5615cc557120 src/HOL/Tools/smallvalue_generators.ML
--- a/src/HOL/Tools/smallvalue_generators.ML	Mon Nov 22 10:42:01 2010 +0100
+++ b/src/HOL/Tools/smallvalue_generators.ML	Mon Nov 22 10:42:03 2010 +0100
@@ -156,8 +156,8 @@
     fun pat_completeness_auto ctxt =
       Pat_Completeness.pat_completeness_tac ctxt 1
       THEN auto_tac (clasimpset_of ctxt)
-  in
-    (thy
+  in 
+    thy
     |> Class.instantiation (tycos, vs, @{sort full_small})
     |> Function.add_function
       (map (fn (T, (name, _)) =>
@@ -168,12 +168,11 @@
     |> Local_Theory.restore
     |> (fn lthy => Function.prove_termination NONE (termination_tac lthy) lthy)
     |> snd
-    |> Class.prove_instantiation_exit (K (Class.intro_classes_tac [])))
-    handle FUNCTION_TYPE =>
+    |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
+  end handle FUNCTION_TYPE =>
     (Datatype_Aux.message config
       "Creation of smallvalue generators failed because the datatype contains a function type";
     thy)
-  end;
 
 (** building and compiling generator expressions **)