src/HOL/Tools/Predicate_Compile/code_prolog.ML
changeset 40924 a9be7f26b4e6
parent 40301 bf39a257b3d3
child 41067 c78a2d402736
     1.1 --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Fri Dec 03 08:40:47 2010 +0100
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Fri Dec 03 08:40:47 2010 +0100
     1.3 @@ -38,7 +38,7 @@
     1.4    val write_program : logic_program -> string
     1.5    val run : (Time.time * prolog_system) -> logic_program -> (string * prol_term list) -> string list -> int option -> prol_term list list
     1.6    
     1.7 -  val quickcheck : Proof.context -> term -> int -> term list option * (bool list * bool)
     1.8 +  val quickcheck : Proof.context -> term -> int -> term list option * Quickcheck.report option
     1.9  
    1.10    val trace : bool Unsynchronized.ref
    1.11    
    1.12 @@ -129,8 +129,8 @@
    1.13  
    1.14  (* general string functions *)
    1.15  
    1.16 -val first_upper = implode o nth_map 0 Symbol.to_ascii_upper o explode;
    1.17 -val first_lower = implode o nth_map 0 Symbol.to_ascii_lower o explode;
    1.18 +val first_upper = implode o nth_map 0 Symbol.to_ascii_upper o raw_explode;
    1.19 +val first_lower = implode o nth_map 0 Symbol.to_ascii_lower o raw_explode;
    1.20  
    1.21  (* internal program representation *)
    1.22  
    1.23 @@ -835,7 +835,7 @@
    1.24  
    1.25  val parse_term = fst o Scan.finite Symbol.stopper
    1.26      (Scan.error (!! (fn _ => raise Fail "parsing prolog output failed")) scan_term)
    1.27 -  o explode
    1.28 +  o raw_explode
    1.29    
    1.30  fun parse_solutions sol =
    1.31    let
    1.32 @@ -1030,9 +1030,8 @@
    1.33        case tss of
    1.34          [ts] => SOME (map (restore_term ctxt' constant_table) (ts ~~ map snd vs'))
    1.35        | _ => NONE
    1.36 -    val empty_report = ([], false)
    1.37    in
    1.38 -    (res, empty_report)
    1.39 +    (res, NONE)
    1.40    end; 
    1.41  
    1.42  end;