--- a/src/HOL/Modelcheck/MuckeSyn.ML Tue Dec 20 08:38:43 2005 +0100
+++ b/src/HOL/Modelcheck/MuckeSyn.ML Tue Dec 20 08:58:36 2005 +0100
@@ -110,14 +110,10 @@
local
-fun is_prefix [] s = true
-| is_prefix (p::ps) [] = false
-| is_prefix (p::ps) (x::xs) = (p=x) andalso (is_prefix ps xs);
-
fun delete_bold [] = []
-| delete_bold (x::xs) = if (is_prefix ("\^["::"["::"0"::"m"::[]) (x::xs))
+| delete_bold (x::xs) = if (is_prefix (op =) ("\^["::"["::"0"::"m"::[]) (x::xs))
then (let val (_::_::_::s) = xs in delete_bold s end)
- else (if (is_prefix ("\^["::"["::"1"::"m"::[]) (x::xs))
+ else (if (is_prefix (op =) ("\^["::"["::"1"::"m"::[]) (x::xs))
then (let val (_::_::_::s) = xs in delete_bold s end)
else (x::delete_bold xs));
--- a/src/HOL/Modelcheck/mucke_oracle.ML Tue Dec 20 08:38:43 2005 +0100
+++ b/src/HOL/Modelcheck/mucke_oracle.ML Tue Dec 20 08:58:36 2005 +0100
@@ -523,7 +523,7 @@
(* "true" stand at the end of the output. *)
local
-infix is_prefix_of contains at_post string_contains string_at_post;
+infix contains at_post string_contains string_at_post;
val is_blank : string -> bool =
fn " " => true | "\t" => true | "\n" => true | "\^L" => true
@@ -537,13 +537,9 @@
fun delete_blanks_string s = implode(delete_blanks (explode s));
- fun [] is_prefix_of s = true
- | (p::ps) is_prefix_of [] = false
- | (p::ps) is_prefix_of (x::xs) = (p = x) andalso (ps is_prefix_of xs);
-
fun [] contains [] = true
| [] contains s = false
- | (x::xs) contains s = (s is_prefix_of (x::xs)) orelse (xs contains s);
+ | (x::xs) contains s = (is_prefix (op =) s (x::xs)) orelse (xs contains s);
fun [] at_post [] = true
| [] at_post s = false
--- a/src/HOL/Tools/ATP/recon_parse.ML Tue Dec 20 08:38:43 2005 +0100
+++ b/src/HOL/Tools/ATP/recon_parse.ML Tue Dec 20 08:58:36 2005 +0100
@@ -73,15 +73,12 @@
exception NOCUT
- fun is_prefix [] l = true
- | is_prefix (h::t) [] = false
- | is_prefix (h::t) (h'::t') = (h = h') andalso is_prefix t t'
fun remove_prefix [] l = l
| remove_prefix (h::t) [] = error "can't remove prefix"
| remove_prefix (h::t) (h'::t') = remove_prefix t t'
fun ccut t [] = raise NOCUT
| ccut t s =
- if is_prefix t s then ([], remove_prefix t s) else
+ if is_prefix (op =) t s then ([], remove_prefix t s) else
let val (a, b) = ccut t (tl s) in ((hd s)::a, b) end
fun cut t s =
let
--- a/src/HOLCF/IOA/Modelcheck/MuIOA.ML Tue Dec 20 08:38:43 2005 +0100
+++ b/src/HOLCF/IOA/Modelcheck/MuIOA.ML Tue Dec 20 08:58:36 2005 +0100
@@ -94,14 +94,10 @@
TransA sg t =
error("malformed automaton def for TransA:\n" ^ (Sign.string_of_term sg t));
-fun is_prefix [] s = true
-| is_prefix (p::ps) [] = false
-| is_prefix (p::ps) (x::xs) = (p=x) andalso (is_prefix ps xs);
-
fun delete_ul [] = []
-| delete_ul (x::xs) = if (is_prefix ("\^["::"["::"4"::"m"::[]) (x::xs))
+| delete_ul (x::xs) = if (is_prefix (op =) ("\^["::"["::"4"::"m"::[]) (x::xs))
then (let val (_::_::_::s) = xs in delete_ul s end)
- else (if (is_prefix ("\^["::"["::"0"::"m"::[]) (x::xs))
+ else (if (is_prefix (op =) ("\^["::"["::"0"::"m"::[]) (x::xs))
then (let val (_::_::_::s) = xs in delete_ul s end)
else (x::delete_ul xs));
--- a/src/HOLCF/IOA/meta_theory/ioa_package.ML Tue Dec 20 08:38:43 2005 +0100
+++ b/src/HOLCF/IOA/meta_theory/ioa_package.ML Tue Dec 20 08:58:36 2005 +0100
@@ -62,13 +62,10 @@
fun extract_constrs thy [] = [] |
extract_constrs thy (a::r) =
let
-fun is_prefix [] s = true
-| is_prefix (p::ps) [] = false
-| is_prefix (p::ps) (x::xs) = (p=x) andalso (is_prefix ps xs);
fun delete_bold [] = []
-| delete_bold (x::xs) = if (is_prefix ("\^["::"["::"1"::"m"::[]) (x::xs))
+| delete_bold (x::xs) = if (is_prefix (op =) ("\^["::"["::"1"::"m"::[]) (x::xs))
then (let val (_::_::_::s) = xs in delete_bold s end)
- else (if (is_prefix ("\^["::"["::"0"::"m"::[]) (x::xs))
+ else (if (is_prefix (op =) ("\^["::"["::"0"::"m"::[]) (x::xs))
then (let val (_::_::_::s) = xs in delete_bold s end)
else (x::delete_bold xs));
fun delete_bold_string s = implode(delete_bold(explode s));