# HG changeset patch
# User wenzelm
# Date 1153855092 -7200
# Node ID 2842450d0eee67b2b2f430b3235ba459910ce79c
# Parent  91443392768787ebd5cdc9857d7911edd55ea80b
avoid Term.is_funtype;

diff -r 914433927687 -r 2842450d0eee src/Pure/Tools/codegen_simtype.ML
--- a/src/Pure/Tools/codegen_simtype.ML	Tue Jul 25 21:18:11 2006 +0200
+++ b/src/Pure/Tools/codegen_simtype.ML	Tue Jul 25 21:18:12 2006 +0200
@@ -24,9 +24,7 @@
     val absi = prep_term thy raw_absi;
     val (repe, repe_ty) = (dest_Const o prep_term thy) raw_repe;
     val repe_ty' = (snd o strip_type) repe_ty;
-    fun dest_fun (ty as Type (_, [ty1, ty2])) =
-          if is_funtype ty then (ty1, ty2)
-          else raise TYPE ("dest_fun", [ty], [])
+    fun dest_fun (Type ("fun", [ty1, ty2])) = (ty1, ty2)
       | dest_fun ty = raise TYPE ("dest_fun", [ty], []);
     val PROP = ObjectLogic.ensure_propT thy
     val (ty_abs, ty_rep) = (dest_fun o fastype_of) repm;