src/HOL/Tools/Function/lexicographic_order.ML
changeset 60781 2da59cdf531c
parent 60752 b48830b670a1
child 67149 e61557884799
     1.1 --- a/src/HOL/Tools/Function/lexicographic_order.ML	Sat Jul 25 23:15:37 2015 +0200
     1.2 +++ b/src/HOL/Tools/Function/lexicographic_order.ML	Sat Jul 25 23:41:53 2015 +0200
     1.3 @@ -201,7 +201,7 @@
     1.4    
     1.5          in (* 4: proof reconstruction *)
     1.6            st |>
     1.7 -          (PRIMITIVE (cterm_instantiate [apply2 (Thm.cterm_of ctxt) (rel, relation)])
     1.8 +          (PRIMITIVE (infer_instantiate ctxt [(#1 (dest_Var rel), Thm.cterm_of ctxt relation)])
     1.9              THEN (REPEAT (resolve_tac ctxt @{thms wf_mlex} 1))
    1.10              THEN (resolve_tac ctxt @{thms wf_empty} 1)
    1.11              THEN EVERY (map (prove_row_tac ctxt) clean_table))