src/HOL/Tools/Function/measure_functions.ML
changeset 59621 291934bac95e
parent 59582 0fbed69ff081
child 67149 e61557884799
     1.1 --- a/src/HOL/Tools/Function/measure_functions.ML	Fri Mar 06 14:01:08 2015 +0100
     1.2 +++ b/src/HOL/Tools/Function/measure_functions.ML	Fri Mar 06 15:58:56 2015 +0100
     1.3 @@ -20,7 +20,7 @@
     1.4  fun find_measures ctxt T =
     1.5    DEPTH_SOLVE (resolve_tac ctxt (rev (Named_Theorems.get ctxt @{named_theorems measure_function})) 1)
     1.6      (HOLogic.mk_Trueprop (mk_is_measure (Var (("f",0), T --> HOLogic.natT)))
     1.7 -     |> Proof_Context.cterm_of ctxt |> Goal.init)
     1.8 +     |> Thm.cterm_of ctxt |> Goal.init)
     1.9    |> Seq.map (Thm.prop_of #> (fn _ $ (_ $ (_ $ f)) => f))
    1.10    |> Seq.list_of
    1.11