src/HOL/Tools/smallvalue_generators.ML
changeset 40641 5615cc557120
parent 40640 3fa1c2472568
child 40644 0850a2a16dce
     1.1 --- a/src/HOL/Tools/smallvalue_generators.ML	Mon Nov 22 10:42:01 2010 +0100
     1.2 +++ b/src/HOL/Tools/smallvalue_generators.ML	Mon Nov 22 10:42:03 2010 +0100
     1.3 @@ -156,8 +156,8 @@
     1.4      fun pat_completeness_auto ctxt =
     1.5        Pat_Completeness.pat_completeness_tac ctxt 1
     1.6        THEN auto_tac (clasimpset_of ctxt)
     1.7 -  in
     1.8 -    (thy
     1.9 +  in 
    1.10 +    thy
    1.11      |> Class.instantiation (tycos, vs, @{sort full_small})
    1.12      |> Function.add_function
    1.13        (map (fn (T, (name, _)) =>
    1.14 @@ -168,12 +168,11 @@
    1.15      |> Local_Theory.restore
    1.16      |> (fn lthy => Function.prove_termination NONE (termination_tac lthy) lthy)
    1.17      |> snd
    1.18 -    |> Class.prove_instantiation_exit (K (Class.intro_classes_tac [])))
    1.19 -    handle FUNCTION_TYPE =>
    1.20 +    |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
    1.21 +  end handle FUNCTION_TYPE =>
    1.22      (Datatype_Aux.message config
    1.23        "Creation of smallvalue generators failed because the datatype contains a function type";
    1.24      thy)
    1.25 -  end;
    1.26  
    1.27  (** building and compiling generator expressions **)
    1.28