# HG changeset patch
# User blanchet
# Date 1301993649 -7200
# Node ID 2088895a37c60d3bf4e854d50967466d3ca232d2
# Parent  89571b08a427119fb272de9f6b708c6e1ea3dc2d
temporarily allow useless encoding of helper facts (e.g. fequal_def) instead of throwing exception

diff -r 89571b08a427 -r 2088895a37c6 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
--- 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)