--- a/src/HOL/Matrix/Compute_Oracle/compute.ML Fri Feb 10 23:12:57 2012 +0100
+++ b/src/HOL/Matrix/Compute_Oracle/compute.ML Fri Feb 10 23:14:23 2012 +0100
@@ -259,8 +259,6 @@
val _ = (case pattern of
AbstractMachine.PVar =>
raise (Make "patterns may not start with a variable")
- (* | AbstractMachine.PConst (_, []) =>
- (print th; raise (Make "no parameter rewrite found"))*)
| _ => ())
(* finally, provide a function for renaming the
@@ -396,7 +394,6 @@
val _ = Theory.assert_super (theory_of computer) thy
val naming = naming_of computer
val (encoding, t) = remove_types (encoding_of computer) t'
- (*val _ = if (!print_encoding) then writeln (makestring ("encoding: ",Encode.fold (fn x => fn s => x::s) encoding [])) else ()*)
val t = runprog (prog_of computer) t
val t = infer_types naming encoding ty t
val eq = Logic.mk_equals (t', t)