--- a/src/HOL/Complex/ex/ReflectedFerrack.thy Thu Sep 18 14:06:58 2008 +0200
+++ b/src/HOL/Complex/ex/ReflectedFerrack.thy Thu Sep 18 19:39:44 2008 +0200
@@ -1997,7 +1997,7 @@
ML {* @{code ferrack_test} () *}
-oracle linr_oracle ("term") = {*
+oracle linr_oracle = {*
let
fun num_of_term vs (t as Free (xn, xT)) = (case AList.lookup (op =) vs t
@@ -2066,11 +2066,14 @@
term_of_fm vs t1 $ term_of_fm vs t2
| term_of_fm vs _ = error "If this is raised, Isabelle/HOL or generate_code is inconsistent.";
-in fn thy => fn t =>
+in fn ct =>
let
+ val thy = Thm.theory_of_cterm ct;
+ val t = Thm.term_of ct;
val fs = term_frees t;
val vs = fs ~~ (0 upto (length fs - 1));
- in HOLogic.mk_Trueprop (HOLogic.mk_eq (t, term_of_fm vs (@{code linrqe} (fm_of_term vs t)))) end
+ val res = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, term_of_fm vs (@{code linrqe} (fm_of_term vs t))));
+ in Thm.cterm_of thy res end
end;
*}