# HG changeset patch
# User wenzelm
# Date 1430229197 -7200
#      Tue Apr 28 15:53:17 2015 +0200
# Node ID 7d523eefe09f67418506d84b9fd2faa0e17dfae1
# Parent  18267ceb10b5d55806af77f89a88ade687e0b10b
test;

diff -r 18267ceb10b5 -r 7d523eefe09f src/Provers/hypsubst.ML
--- a/src/Provers/hypsubst.ML	Tue Apr 28 11:48:44 2015 +0200
+++ b/src/Provers/hypsubst.ML	Tue Apr 28 15:53:17 2015 +0200
@@ -286,7 +286,7 @@
               inst_subst_tac ctxt symopt (if symopt then ssubst else Data.subst) i,
               all_imp_intr_tac ctxt hyps i])
   end
-  handle THM _ => no_tac | EQ_VAR => no_tac);
+  handle TERM _ => no_tac | THM _ => no_tac | EQ_VAR => no_tac);
 
 (*apply an equality or definition ONCE;
   fails unless the substitution has an effect*)