--- a/src/Pure/Isar/obtain.ML Mon Jun 15 10:25:49 2015 +0200
+++ b/src/Pure/Isar/obtain.ML Mon Jun 15 10:33:37 2015 +0200
@@ -93,8 +93,13 @@
local
val mk_all_external = Logic.all_constraint o Variable.default_type;
-fun mk_all_internal _ (y, z) t =
- let val T = the (AList.lookup (op =) (Term.add_frees t []) z);
+
+fun mk_all_internal ctxt (y, z) t =
+ let
+ val T =
+ (case AList.lookup (op =) (Term.add_frees t []) z of
+ SOME T => T
+ | NONE => the_default dummyT (Variable.default_type ctxt z));
in Logic.all_const T $ Term.lambda_name (y, Free (z, T)) t end;
fun prepare_clause prep_var parse_prop mk_all ctxt thesis raw_vars raw_props =