src/Pure/Proof/extraction.ML
changeset 21858 05f57309170c
parent 21646 c07b5b0e8492
child 22360 26ead7ed4f4b
     1.1 --- a/src/Pure/Proof/extraction.ML	Thu Dec 14 22:19:39 2006 +0100
     1.2 +++ b/src/Pure/Proof/extraction.ML	Fri Dec 15 00:08:06 2006 +0100
     1.3 @@ -315,7 +315,7 @@
     1.4    in fn (thm, (vs, s1, s2)) =>
     1.5      let
     1.6        val name = Thm.get_name thm;
     1.7 -      val _ = assert (name <> "") "add_realizers: unnamed theorem";
     1.8 +      val _ = name <> "" orelse error "add_realizers: unnamed theorem";
     1.9        val prop = Pattern.rewrite_term thy'
    1.10          (map (Logic.dest_equals o prop_of) defs) [] (prop_of thm);
    1.11        val vars = vars_of prop;
    1.12 @@ -360,7 +360,7 @@
    1.13        defs, expand, prep} = ExtractionData.get thy;
    1.14  
    1.15      val name = Thm.get_name thm;
    1.16 -    val _ = assert (name <> "") "add_expand_thms: unnamed theorem";
    1.17 +    val _ = name <> "" orelse error "add_expand_thms: unnamed theorem";
    1.18  
    1.19      val is_def =
    1.20        (case strip_comb (fst (Logic.dest_equals (prop_of thm))) of
    1.21 @@ -568,7 +568,7 @@
    1.22                NONE => (case find vs' (find' name defs') of
    1.23                  NONE =>
    1.24                    let
    1.25 -                    val _ = assert (T = nullT) "corr: internal error";
    1.26 +                    val _ = T = nullT orelse error "corr: internal error";
    1.27                      val _ = msg d ("Building correctness proof for " ^ quote name ^
    1.28                        (if null vs' then ""
    1.29                         else " (relevant variables: " ^ commas_quote vs' ^ ")"));
    1.30 @@ -720,8 +720,8 @@
    1.31        let
    1.32          val {prop, der = (_, prf), sign, ...} = rep_thm thm;
    1.33          val name = Thm.get_name thm;
    1.34 -        val _ = assert (name <> "") "extraction: unnamed theorem";
    1.35 -        val _ = assert (etype_of thy' vs [] prop <> nullT) ("theorem " ^
    1.36 +        val _ = name <> "" orelse error "extraction: unnamed theorem";
    1.37 +        val _ = etype_of thy' vs [] prop <> nullT orelse error ("theorem " ^
    1.38            quote name ^ " has no computational content")
    1.39        in (Reconstruct.reconstruct_proof sign prop prf, vs) end;
    1.40