equal
deleted
inserted
replaced
426 Bound 0 $ @{term "None :: term list option"} $ return) |
426 Bound 0 $ @{term "None :: term list option"} $ return) |
427 in HOLogic.mk_comp (wrap, mk_validator_expr ctxt t) end |
427 in HOLogic.mk_comp (wrap, mk_validator_expr ctxt t) end |
428 |
428 |
429 (** generator compiliation **) |
429 (** generator compiliation **) |
430 |
430 |
|
431 (* FIXME just one data slot (record) per program unit *) |
|
432 |
431 structure Counterexample = Proof_Data |
433 structure Counterexample = Proof_Data |
432 ( |
434 ( |
433 type T = unit -> int -> bool -> int -> (bool * term list) option |
435 type T = unit -> int -> bool -> int -> (bool * term list) option |
434 (* FIXME avoid user error with non-user text *) |
436 (* FIXME avoid user error with non-user text *) |
435 fun init _ () = error "Counterexample" |
437 fun init _ () = error "Counterexample" |