diff -r fc41a5650fb1 -r c821f1f3d92d src/HOL/Tools/Function/function_context_tree.ML
--- a/src/HOL/Tools/Function/function_context_tree.ML	Thu Apr 06 21:37:13 2017 +0200
+++ b/src/HOL/Tools/Function/function_context_tree.ML	Fri Apr 07 10:56:41 2017 +0200
@@ -16,7 +16,7 @@
   val cong_add: attribute
   val cong_del: attribute
 
-  val mk_tree: (string * typ) -> term -> Proof.context -> term -> ctx_tree
+  val mk_tree: term -> term -> Proof.context -> term -> ctx_tree
 
   val inst_tree: Proof.context -> term -> term -> ctx_tree -> ctx_tree
 
@@ -114,7 +114,7 @@
      (let
         val thy = Proof_Context.theory_of ctxt
 
-        val tt' = Logic.mk_equals (Pattern.rewrite_term thy [(Free fvar, h)] [] t, t)
+        val tt' = Logic.mk_equals (Pattern.rewrite_term thy [(fvar, h)] [] t, t)
         val (c, subs) = (Thm.concl_of r, Thm.prems_of r)
 
         val subst = Pattern.match thy (c, tt') (Vartab.empty, Vartab.empty)
@@ -135,14 +135,14 @@
     (* FIXME: Save in theory: *)
     val congs_deps = map (fn c => (c, cong_deps c)) (congs @ default_congs)
 
-    fun matchcall (a $ b) = if a = Free fvar then SOME b else NONE
+    fun matchcall (a $ b) = if a = fvar then SOME b else NONE
       | matchcall _ = NONE
 
     fun mk_tree' ctxt t =
       case matchcall t of
         SOME arg => RCall (t, mk_tree' ctxt arg)
       | NONE =>
-        if not (exists_subterm (fn Free v => v = fvar | _ => false) t) then Leaf t
+        if not (exists_subterm (fn v => v = fvar) t) then Leaf t
         else
           let
             val (r, dep, branches) = find_cong_rule ctxt fvar h congs_deps t