Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Function/measure_functions.ML
changeset 42361 23f352990944
parent 38764 e6a18808873c
child 45294 3c5d3d286055 
--- a/src/HOL/Tools/Function/measure_functions.ML	Sat Apr 16 15:47:52 2011 +0200
+++ b/src/HOL/Tools/Function/measure_functions.ML	Sat Apr 16 16:15:37 2011 +0200
@@ -29,7 +29,7 @@
 fun find_measures ctxt T =
   DEPTH_SOLVE (resolve_tac (Measure_Heuristic_Rules.get ctxt) 1)
     (HOLogic.mk_Trueprop (mk_is_measure (Var (("f",0), T --> HOLogic.natT)))
-     |> cterm_of (ProofContext.theory_of ctxt) |> Goal.init)
+     |> cterm_of (Proof_Context.theory_of ctxt) |> Goal.init)
   |> Seq.map (prop_of #> (fn _ $ (_ $ (_ $ f)) => f))
   |> Seq.list_of
isabelle