Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
avoid Term.is_funtype;
authorwenzelm
Tue, 25 Jul 2006 21:18:12 +0200
changeset 20204 2842450d0eee
parent 20203 914433927687
child 20205 7b2958d3d575
avoid Term.is_funtype;
src/Pure/Tools/codegen_simtype.ML file | annotate | diff | comparison | revisions 
--- 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;
isabelle