--- a/src/HOL/Bali/AxExample.thy Wed Sep 14 01:47:06 2005 +0200
+++ b/src/HOL/Bali/AxExample.thy Wed Sep 14 10:13:12 2005 +0200
@@ -40,7 +40,7 @@
declare lvar_def [simp]
ML {*
-fun inst1_tac s t st = case assoc (rev (term_varnames (prop_of st)), s) of
+fun inst1_tac s t st = case AList.lookup (op =) (rev (term_varnames (prop_of st))) s of
SOME i => Tactic.instantiate_tac' [((s, i), t)] st | NONE => Seq.empty;
val ax_tac = REPEAT o rtac allI THEN'
resolve_tac(thm "ax_Skip"::thm "ax_StatRef"::thm "ax_MethdN"::
--- a/src/HOL/Modelcheck/mucke_oracle.ML Wed Sep 14 01:47:06 2005 +0200
+++ b/src/HOL/Modelcheck/mucke_oracle.ML Wed Sep 14 10:13:12 2005 +0200
@@ -255,9 +255,8 @@
let val v = variant used (string_of_indexname ix)
in ((ix,v)::pairs, v::used) end;
val (alist, _) = foldr newName ([], used) vars;
- fun mk_inst (Var(v,T)) =
- (Var(v,T),
- Free(valOf (assoc(alist,v)), T));
+ fun mk_inst (Var(v,T)) = (Var(v,T),
+ Free ((the o AList.lookup (op =) alist) v, T));
val insts = map mk_inst vars;
in subst_atomic insts t end;
--- a/src/HOL/Tools/ATP/recon_translate_proof.ML Wed Sep 14 01:47:06 2005 +0200
+++ b/src/HOL/Tools/ATP/recon_translate_proof.ML Wed Sep 14 10:13:12 2005 +0200
@@ -89,7 +89,7 @@
(************************************************)
fun follow_axiom clauses allvars (clausenum:int) thml clause_strs =
- let val this_axiom = valOf (assoc (clauses,clausenum))
+ let val this_axiom = (the o AList.lookup (op =) clauses) clausenum
val (res, numlist, symlist, nsymlist) = (ReconOrderClauses.rearrange_clause this_axiom clause_strs allvars)
val thmvars = thm_vars res
in
@@ -103,8 +103,8 @@
(* numbers of clauses and literals*) (*vars*) (*list of current thms*) (* literal strings as parsed from spass *)
fun follow_binary ((clause1, lit1), (clause2 , lit2)) allvars thml clause_strs =
- let val thm1 = select_literal (lit1 + 1) (valOf (assoc (thml,clause1)))
- val thm2 = valOf (assoc (thml,clause2))
+ let val thm1 = select_literal (lit1 + 1) ((the o AList.lookup (op =) thml) clause1)
+ val thm2 = (the o AList.lookup (op =) thml) clause2
val res = thm1 RSN ((lit2 +1), thm2)
val (res', numlist, symlist, nsymlist) = (ReconOrderClauses.rearrange_clause res clause_strs allvars)
val thmvars = thm_vars res
@@ -121,8 +121,8 @@
fun follow_mrr ((clause1, lit1), (clause2 , lit2)) allvars thml clause_strs =
- let val thm1 = select_literal (lit1 + 1) (valOf (assoc (thml,clause1)))
- val thm2 = valOf (assoc (thml,clause2))
+ let val thm1 = select_literal (lit1 + 1) ((the o AList.lookup (op =) thml) clause1)
+ val thm2 = (the o AList.lookup (op =) thml) clause2
val res = thm1 RSN ((lit2 +1), thm2)
val (res', numlist, symlist, nsymlist) =
(ReconOrderClauses.rearrange_clause res clause_strs allvars)
@@ -169,7 +169,7 @@
(*FIXME: share code with that in Tools/reconstruction.ML*)
fun follow_factor clause lit1 lit2 allvars thml clause_strs =
let
- val th = valOf (assoc (thml,clause))
+ val th = (the o AList.lookup (op =) thml) clause
val prems = prems_of th
val sign = sign_of_thm th
val fac1 = ReconOrderClauses.get_nth (lit1+1) prems
@@ -237,8 +237,8 @@
fun follow_standard_para ((clause1, lit1), (clause2 , lit2)) allvars thml clause_strs =
let
- val th1 = valOf (assoc (thml,clause1))
- val th2 = valOf (assoc (thml,clause2))
+ val th1 = (the o AList.lookup (op =) thml) clause1
+ val th2 = (the o AList.lookup (op =) thml) clause2
val eq_lit_th = select_literal (lit1+1) th1
val mod_lit_th = select_literal (lit2+1) th2
val eqsubst = eq_lit_th RSN (2,rev_subst)
@@ -295,8 +295,8 @@
(* changed negate_nead to negate_head here too*)
(* clause1, lit1 is thing to rewrite with *)
(*fun follow_rewrite ((clause1, lit1), (clause2, lit2)) allvars thml clause_strs =
- let val th1 = valOf (assoc (thml,clause1))
- val th2 = valOf (assoc (thml,clause2))
+ let val th1 = (the o AList.lookup (op =) thml) clause1
+ val th2 = (the o AList.lookup (op =) thml) clause2
val eq_lit_th = select_literal (lit1+1) th1
val mod_lit_th = select_literal (lit2+1) th2
val eqsubst = eq_lit_th RSN (2,rev_subst)
@@ -321,7 +321,7 @@
fun follow_obvious (clause1, lit1) allvars thml clause_strs =
- let val th1 = valOf (assoc (thml,clause1))
+ let val th1 = (the o AList.lookup (op =) thml) clause1
val prems1 = prems_of th1
val newthm = refl RSN ((lit1+ 1), th1)
handle THM _ => hd (Seq.list_of(delete_assump_tac th1 (lit1 + 1)))