diff -r a6e977d8b070 -r bb1e4a35d506 src/HOL/Tools/Function/pat_completeness.ML
--- a/src/HOL/Tools/Function/pat_completeness.ML	Fri Mar 06 21:14:27 2015 +0100
+++ b/src/HOL/Tools/Function/pat_completeness.ML	Fri Mar 06 21:20:30 2015 +0100
@@ -23,10 +23,10 @@
 
 fun inst_free var inst = Thm.forall_elim inst o Thm.forall_intr var
 
-fun inst_case_thm thy x P thm =
+fun inst_case_thm ctxt x P thm =
   let val [Pv, xv] = Term.add_vars (Thm.prop_of thm) []
   in
-    thm |> cterm_instantiate (map (apply2 (Thm.global_cterm_of thy)) [(Var xv, x), (Var Pv, P)])
+    thm |> cterm_instantiate (map (apply2 (Thm.cterm_of ctxt)) [(Var xv, x), (Var Pv, P)])
   end
 
 fun invent_vars constr i =
@@ -40,26 +40,24 @@
    (avs, pvs, j)
  end
 
-fun filter_pats ctxt cons pvars [] = []
-  | filter_pats ctxt cons pvars (([], thm) :: pts) = raise Match
+fun filter_pats _ _ _ [] = []
+  | filter_pats _ _ _ (([], _) :: _) = raise Match
   | filter_pats ctxt cons pvars (((pat as Free _) :: pats, thm) :: pts) =
-    let val inst = list_comb (cons, pvars) in
-      (inst :: pats,
-        inst_free (Thm.cterm_of ctxt pat) (Thm.cterm_of ctxt inst) thm)
-        :: (filter_pats ctxt cons pvars pts)
-    end
-  | filter_pats thy cons pvars ((pat :: pats, thm) :: pts) =
-    if fst (strip_comb pat) = cons
-    then (pat :: pats, thm) :: (filter_pats thy cons pvars pts)
-    else filter_pats thy cons pvars pts
+      let val inst = list_comb (cons, pvars) in
+        (inst :: pats, inst_free (Thm.cterm_of ctxt pat) (Thm.cterm_of ctxt inst) thm) ::
+          filter_pats ctxt cons pvars pts
+      end
+  | filter_pats ctxt cons pvars ((pat :: pats, thm) :: pts) =
+      if fst (strip_comb pat) = cons
+      then (pat :: pats, thm) :: filter_pats ctxt cons pvars pts
+      else filter_pats ctxt cons pvars pts
 
 
-fun transform_pat _ avars c_assum ([] , thm) = raise Match
+fun transform_pat _ _ _ ([] , _) = raise Match
   | transform_pat ctxt avars c_assum (pat :: pats, thm) =
       let
         val (_, subps) = strip_comb pat
-        val eqs =
-          map (Thm.cterm_of ctxt o HOLogic.mk_Trueprop o HOLogic.mk_eq) (avars ~~ subps)
+        val eqs = map (Thm.cterm_of ctxt o HOLogic.mk_Trueprop o HOLogic.mk_eq) (avars ~~ subps)
         val c_eq_pat =
           simplify (put_simpset HOL_basic_ss ctxt addsimps (map Thm.assume eqs)) c_assum
       in
@@ -95,13 +93,12 @@
                   (Thm.cterm_of ctxt v) thm))) pts)
       else (* Cons case *)
         let
-          val thy = Proof_Context.theory_of ctxt
           val T as Type (tname, _) = fastype_of v
           val SOME {exhaust=case_thm, ...} = Ctr_Sugar.ctr_sugar_of ctxt tname
           val constrs = inst_constrs_of ctxt T
           val c_cases = map (constr_case ctxt P idx (v :: vs) pts) constrs
         in
-          inst_case_thm thy v P case_thm
+          inst_case_thm ctxt v P case_thm
           |> fold (curry op COMP) c_cases
         end
   | o_alg _ _ _ _ _ = raise Match