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.
temporarily allow useless encoding of helper facts (e.g. fequal_def) instead of throwing exception
authorblanchet
Tue, 05 Apr 2011 10:54:09 +0200
changeset 42236 2088895a37c6
parent 42235 89571b08a427
child 42237 e645d7255bd4
temporarily allow useless encoding of helper facts (e.g. fequal_def) instead of throwing exception
src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Tue Apr 05 10:47:37 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Tue Apr 05 10:54:09 2011 +0200
@@ -405,9 +405,11 @@
 val mangled_type_sep = "\000"
 
 fun mangled_combtyp f (CombTFree name) = f name
+  | mangled_combtyp f (CombTVar name) =
+    f name (* FIXME: shouldn't happen *)
+    (* raise Fail "impossible schematic type variable" *)
   | mangled_combtyp f (CombType (name, tys)) =
     "(" ^ commas (map (mangled_combtyp f) tys) ^ ")" ^ f name
-  | mangled_combtyp _ _ = raise Fail "impossible schematic type variable"
 
 fun mangled_type_suffix f g tys =
   fold_rev (curry (op ^) o g o prefix mangled_type_sep o mangled_combtyp f)
isabelle