# HG changeset patch
# User wenzelm
# Date 1418990166 -3600
# Node ID a012574b78e7581316eb5677f2635f0a5fb930e1
# Parent  71b416020f423fbc480c215d32011364fb71cce4
proper exception for internal program failure, not user-error;

diff -r 71b416020f42 -r a012574b78e7 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Dec 19 12:36:50 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Dec 19 12:56:06 2014 +0100
@@ -1687,56 +1687,49 @@
 structure Pred_Result = Proof_Data
 (
   type T = unit -> term Predicate.pred
-  (* FIXME avoid user error with non-user text *)
-  fun init _ () = error "Pred_Result"
+  fun init _ () = raise Fail "Pred_Result"
 );
 val put_pred_result = Pred_Result.put;
 
 structure Pred_Random_Result = Proof_Data
 (
   type T = unit -> seed -> term Predicate.pred * seed
-  (* FIXME avoid user error with non-user text *)
-  fun init _ () = error "Pred_Random_Result"
+  fun init _ () = raise Fail "Pred_Random_Result"
 );
 val put_pred_random_result = Pred_Random_Result.put;
 
 structure Dseq_Result = Proof_Data
 (
   type T = unit -> term Limited_Sequence.dseq
-  (* FIXME avoid user error with non-user text *)
-  fun init _ () = error "Dseq_Result"
+  fun init _ () = raise Fail "Dseq_Result"
 );
 val put_dseq_result = Dseq_Result.put;
 
 structure Dseq_Random_Result = Proof_Data
 (
   type T = unit -> Code_Numeral.natural -> Code_Numeral.natural -> seed -> term Limited_Sequence.dseq * seed
-  (* FIXME avoid user error with non-user text *)
-  fun init _ () = error "Dseq_Random_Result"
+  fun init _ () = raise Fail "Dseq_Random_Result"
 );
 val put_dseq_random_result = Dseq_Random_Result.put;
 
 structure New_Dseq_Result = Proof_Data
 (
   type T = unit -> Code_Numeral.natural -> term Lazy_Sequence.lazy_sequence
-  (* FIXME avoid user error with non-user text *)
-  fun init _ () = error "New_Dseq_Random_Result"
+  fun init _ () = raise Fail "New_Dseq_Random_Result"
 );
 val put_new_dseq_result = New_Dseq_Result.put;
 
 structure Lseq_Random_Result = Proof_Data
 (
   type T = unit -> Code_Numeral.natural -> Code_Numeral.natural -> seed -> Code_Numeral.natural -> term Lazy_Sequence.lazy_sequence
-  (* FIXME avoid user error with non-user text *)
-  fun init _ () = error "Lseq_Random_Result"
+  fun init _ () = raise Fail "Lseq_Random_Result"
 );
 val put_lseq_random_result = Lseq_Random_Result.put;
 
 structure Lseq_Random_Stats_Result = Proof_Data
 (
   type T = unit -> Code_Numeral.natural -> Code_Numeral.natural -> seed -> Code_Numeral.natural -> (term * Code_Numeral.natural) Lazy_Sequence.lazy_sequence
-  (* FIXME avoid user error with non-user text *)
-  fun init _ () = error "Lseq_Random_Stats_Result"
+  fun init _ () = raise Fail "Lseq_Random_Stats_Result"
 );
 val put_lseq_random_stats_result = Lseq_Random_Stats_Result.put;
 
diff -r 71b416020f42 -r a012574b78e7 src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Fri Dec 19 12:36:50 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Fri Dec 19 12:56:06 2014 +0100
@@ -44,41 +44,39 @@
 
 structure Pred_Result = Proof_Data
 (
-  type T = unit -> Code_Numeral.natural -> Code_Numeral.natural -> Code_Numeral.natural -> seed -> term list Predicate.pred
-  (* FIXME avoid user error with non-user text *)
-  fun init _ () = error "Pred_Result"
+  type T = unit -> Code_Numeral.natural -> Code_Numeral.natural ->
+    Code_Numeral.natural -> seed -> term list Predicate.pred
+  fun init _ () = raise Fail "Pred_Result"
 )
 val put_pred_result = Pred_Result.put
 
 structure Dseq_Result = Proof_Data
 (
-  type T = unit -> Code_Numeral.natural -> Code_Numeral.natural -> seed -> term list Limited_Sequence.dseq * seed
-  (* FIXME avoid user error with non-user text *)
-  fun init _ () = error "Dseq_Result"
+  type T = unit -> Code_Numeral.natural -> Code_Numeral.natural ->
+    seed -> term list Limited_Sequence.dseq * seed
+  fun init _ () = raise Fail "Dseq_Result"
 )
 val put_dseq_result = Dseq_Result.put
 
 structure Lseq_Result = Proof_Data
 (
-  type T = unit -> Code_Numeral.natural -> Code_Numeral.natural -> seed -> Code_Numeral.natural -> term list Lazy_Sequence.lazy_sequence
-  (* FIXME avoid user error with non-user text *)
-  fun init _ () = error "Lseq_Result"
+  type T = unit -> Code_Numeral.natural -> Code_Numeral.natural ->
+    seed -> Code_Numeral.natural -> term list Lazy_Sequence.lazy_sequence
+  fun init _ () = raise Fail "Lseq_Result"
 )
 val put_lseq_result = Lseq_Result.put
 
 structure New_Dseq_Result = Proof_Data
 (
   type T = unit -> Code_Numeral.natural -> term list Lazy_Sequence.lazy_sequence
-  (* FIXME avoid user error with non-user text *)
-  fun init _ () = error "New_Dseq_Random_Result"
+  fun init _ () = raise Fail "New_Dseq_Random_Result"
 )
 val put_new_dseq_result = New_Dseq_Result.put
 
 structure CPS_Result = Proof_Data
 (
   type T = unit -> Code_Numeral.natural -> (bool * term list) option
-  (* FIXME avoid user error with non-user text *)
-  fun init _ () = error "CPS_Result"
+  fun init _ () = raise Fail "CPS_Result"
 )
 val put_cps_result = CPS_Result.put
 
diff -r 71b416020f42 -r a012574b78e7 src/HOL/Tools/Quickcheck/exhaustive_generators.ML
--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Fri Dec 19 12:36:50 2014 +0100
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Fri Dec 19 12:56:06 2014 +0100
@@ -446,25 +446,23 @@
 
 structure Counterexample = Proof_Data
 (
-  type T = unit -> Code_Numeral.natural -> bool -> Code_Numeral.natural -> (bool * term list) option
-  (* FIXME avoid user error with non-user text *)
-  fun init _ () = error "Counterexample"
+  type T = unit -> Code_Numeral.natural -> bool ->
+    Code_Numeral.natural -> (bool * term list) option
+  fun init _ () = raise Fail "Counterexample"
 );
 val put_counterexample = Counterexample.put;
 
 structure Counterexample_Batch = Proof_Data
 (
   type T = unit -> (Code_Numeral.natural -> term list option) list
-  (* FIXME avoid user error with non-user text *)
-  fun init _ () = error "Counterexample"
+  fun init _ () = raise Fail "Counterexample"
 );
 val put_counterexample_batch = Counterexample_Batch.put;
 
 structure Validator_Batch = Proof_Data
 (
   type T = unit -> (Code_Numeral.natural -> bool) list
-  (* FIXME avoid user error with non-user text *)
-  fun init _ () = error "Counterexample"
+  fun init _ () = raise Fail "Counterexample"
 );
 val put_validator_batch = Validator_Batch.put;
 
diff -r 71b416020f42 -r a012574b78e7 src/HOL/Tools/Quickcheck/narrowing_generators.ML
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Dec 19 12:36:50 2014 +0100
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Dec 19 12:56:06 2014 +0100
@@ -315,7 +315,7 @@
 structure Counterexample = Proof_Data
 (
   type T = unit -> (bool * term list) option
-  fun init _ () = error "Counterexample"
+  fun init _ () = raise Fail "Counterexample"
 )
 
 datatype counterexample = Universal_Counterexample of (term * counterexample)
@@ -332,7 +332,7 @@
 structure Existential_Counterexample = Proof_Data
 (
   type T = unit -> counterexample option
-  fun init _ () = error "Counterexample"
+  fun init _ () = raise Fail "Counterexample"
 )
 
 val put_existential_counterexample = Existential_Counterexample.put
diff -r 71b416020f42 -r a012574b78e7 src/HOL/Tools/Quickcheck/random_generators.ML
--- a/src/HOL/Tools/Quickcheck/random_generators.ML	Fri Dec 19 12:36:50 2014 +0100
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Fri Dec 19 12:56:06 2014 +0100
@@ -273,16 +273,14 @@
 structure Counterexample = Proof_Data
 (
   type T = unit -> Code_Numeral.natural -> bool -> Code_Numeral.natural -> seed -> (bool * term list) option * seed
-  (* FIXME avoid user error with non-user text *)
-  fun init _ () = error "Counterexample"
+  fun init _ () = raise Fail "Counterexample"
 );
 val put_counterexample = Counterexample.put;
 
 structure Counterexample_Report = Proof_Data
 (
   type T = unit -> Code_Numeral.natural -> bool -> Code_Numeral.natural -> seed -> ((bool * term list) option * (bool list * bool)) * seed
-  (* FIXME avoid user error with non-user text *)
-  fun init _ () = error "Counterexample_Report"
+  fun init _ () = raise Fail "Counterexample_Report"
 );
 val put_counterexample_report = Counterexample_Report.put;
 
diff -r 71b416020f42 -r a012574b78e7 src/HOL/Tools/code_evaluation.ML
--- a/src/HOL/Tools/code_evaluation.ML	Fri Dec 19 12:36:50 2014 +0100
+++ b/src/HOL/Tools/code_evaluation.ML	Fri Dec 19 12:56:06 2014 +0100
@@ -174,8 +174,7 @@
 structure Evaluation = Proof_Data
 (
   type T = unit -> term
-  (* FIXME avoid user error with non-user text *)
-  fun init _ () = error "Evaluation"
+  fun init _ () = raise Fail "Evaluation"
 );
 val put_term = Evaluation.put;
 val cookie = (Evaluation.get, put_term, "Code_Evaluation.put_term");
diff -r 71b416020f42 -r a012574b78e7 src/Tools/Code/code_runtime.ML
--- a/src/Tools/Code/code_runtime.ML	Fri Dec 19 12:36:50 2014 +0100
+++ b/src/Tools/Code/code_runtime.ML	Fri Dec 19 12:56:06 2014 +0100
@@ -160,8 +160,7 @@
 structure Truth_Result = Proof_Data
 (
   type T = unit -> truth
-  (* FIXME avoid user error with non-user text *)
-  fun init _ () = error "Truth_Result"
+  fun init _ () = raise Fail "Truth_Result"
 );
 val put_truth = Truth_Result.put;
 val truth_cookie = (Truth_Result.get, put_truth, Long_Name.append this "put_truth");
diff -r 71b416020f42 -r a012574b78e7 src/Tools/nbe.ML
--- a/src/Tools/nbe.ML	Fri Dec 19 12:36:50 2014 +0100
+++ b/src/Tools/nbe.ML	Fri Dec 19 12:56:06 2014 +0100
@@ -234,18 +234,17 @@
 structure Univs = Proof_Data
 (
   type T = unit -> Univ list -> Univ list
-  (* FIXME avoid user error with non-user text *)
-  fun init _ () = error "Univs"
+  fun init _ () = raise Fail "Univs"
 );
 val put_result = Univs.put;
 
 local
-  val prefix =     "Nbe.";
-  val name_put =   prefix ^ "put_result";
+  val prefix = "Nbe.";
+  val name_put = prefix ^ "put_result";
   val name_const = prefix ^ "Const";
-  val name_abss =  prefix ^ "abss";
-  val name_apps =  prefix ^ "apps";
-  val name_same =  prefix ^ "same";
+  val name_abss = prefix ^ "abss";
+  val name_apps = prefix ^ "apps";
+  val name_same = prefix ^ "same";
 in
 
 val univs_cookie = (Univs.get, put_result, name_put);