--- a/src/HOL/Matrix/Compute_Oracle/am.ML Sun Feb 12 22:10:33 2012 +0100
+++ b/src/HOL/Matrix/Compute_Oracle/am.ML Fri Feb 10 22:51:21 2012 +0100
@@ -50,13 +50,13 @@
(*Returns true iff at most 0 .. (free-1) occur unbound. therefore
check_freevars 0 t iff t is closed*)
fun check_freevars free (Var x) = x < free
- | check_freevars free (Const c) = true
+ | check_freevars free (Const _) = true
| check_freevars free (App (u, v)) = check_freevars free u andalso check_freevars free v
| check_freevars free (Abs m) = check_freevars (free+1) m
| check_freevars free (Computed t) = check_freevars free t
fun forall_consts pred (Const c) = pred c
- | forall_consts pred (Var x) = true
+ | forall_consts pred (Var _) = true
| forall_consts pred (App (u,v)) = forall_consts pred u
andalso forall_consts pred v
| forall_consts pred (Abs m) = forall_consts pred m
@@ -70,6 +70,6 @@
exception Run of string;
-fun run p t = raise Run "abstract machine stub"
+fun run _ _ = raise Run "abstract machine stub"
end