# HG changeset patch # User haftmann # Date 1126685592 -7200 # Node ID 63e0ab9f2ea95168251bdeee64ed8803918e1c52 # Parent 27509e72f29ee3d6c99f7f4220877c7c82a6c4c4 introduces AList.lookup diff -r 27509e72f29e -r 63e0ab9f2ea9 src/HOL/Bali/AxExample.thy --- 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":: diff -r 27509e72f29e -r 63e0ab9f2ea9 src/HOL/Modelcheck/mucke_oracle.ML --- 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; diff -r 27509e72f29e -r 63e0ab9f2ea9 src/HOL/Tools/ATP/recon_translate_proof.ML --- 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)))