src/HOL/Tools/Function/pat_completeness.ML
changeset 60781 2da59cdf531c
parent 59627 bb1e4a35d506
     1.1 --- a/src/HOL/Tools/Function/pat_completeness.ML	Sat Jul 25 23:15:37 2015 +0200
     1.2 +++ b/src/HOL/Tools/Function/pat_completeness.ML	Sat Jul 25 23:41:53 2015 +0200
     1.3 @@ -24,9 +24,9 @@
     1.4  fun inst_free var inst = Thm.forall_elim inst o Thm.forall_intr var
     1.5  
     1.6  fun inst_case_thm ctxt x P thm =
     1.7 -  let val [Pv, xv] = Term.add_vars (Thm.prop_of thm) []
     1.8 +  let val [P_name, x_name] = Term.add_var_names (Thm.prop_of thm) []
     1.9    in
    1.10 -    thm |> cterm_instantiate (map (apply2 (Thm.cterm_of ctxt)) [(Var xv, x), (Var Pv, P)])
    1.11 +    thm |> infer_instantiate ctxt [(x_name, Thm.cterm_of ctxt x), (P_name, Thm.cterm_of ctxt P)]
    1.12    end
    1.13  
    1.14  fun invent_vars constr i =