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/Tools/Code/code_runtime.ML
changeset 47609 b3dab1892cda
parent 46961 5c6955f487e5
child 48568 084cd758a8ab 
--- a/src/Tools/Code/code_runtime.ML	Thu Apr 19 18:24:40 2012 +0200
+++ b/src/Tools/Code/code_runtime.ML	Thu Apr 19 19:18:11 2012 +0200
@@ -149,7 +149,7 @@
 
 local
 
-fun check_holds thy evaluator vs_t deps ct =
+fun check_holds thy evaluator vs_t ct =
   let
     val t = Thm.term_of ct;
     val _ = if fastype_of t <> propT
@@ -165,10 +165,10 @@
 
 val (_, raw_check_holds_oracle) = Context.>>> (Context.map_theory_result
   (Thm.add_oracle (@{binding holds_by_evaluation},
-  fn (thy, evaluator, vs_t, deps, ct) => check_holds thy evaluator vs_t deps ct)));
+  fn (thy, evaluator, vs_t, ct) => check_holds thy evaluator vs_t ct)));
 
 fun check_holds_oracle thy evaluator ((_, vs_ty), t) deps ct =
-  raw_check_holds_oracle (thy, evaluator, (vs_ty, t), deps, ct);
+  raw_check_holds_oracle (thy, evaluator, (vs_ty, t), ct);
 
 in
isabelle