src/HOL/Tools/Function/function_context_tree.ML

   val add_function_cong : thm -> Context.generic -> Context.generic
 
   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
 
   val export_term : ctxt -> term -> term
   val export_thm : Proof.context -> ctxt -> thm -> thm

 
 fun find_cong_rule ctxt fvar h ((r,dep)::rs) t =
      (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)
         val branches = map (mk_branch ctxt o Envir.beta_norm o Envir.subst_term subst) subs
         val inst =

     val congs = get_function_congs ctxt
 
     (* 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
             fun subtree (ctxt', fixes, assumes, st) =
               ((fixes,