Skip to content
This repository
Browse code

more informative error messages for Opentheory.define_X_in_thy

  • Loading branch information...
commit 9c4ab829de06aeb5d8fbba362039ebe3fd91803c 1 parent 150cdd4
Ramana Kumar authored December 06, 2011

Showing 1 changed file with 10 additions and 6 deletions. Show diff stats Hide diff stats

  1. 16  src/opentheory/Opentheory.sml
16  src/opentheory/Opentheory.sml
@@ -30,19 +30,23 @@ fun define_tyop_in_thy
30 30
   open boolLib
31 31
   val (P,t) = dest_comb (concl ax)
32 32
   val v   = variant (free_vars P) (mk_var ("v",type_of t))
33  
-  val _   = if tthy = current_theory() then () else
34  
-            raise ERR "define_tyop_in_thy" "wrong theory"
  33
+  val ct  = current_theory()
  34
+  val _   = if tthy = ct then () else
  35
+            raise ERR "define_tyop_in_thy" ("wrong theory: "^ct^" (wanted "^tthy^" for "^Tyop^")")
35 36
   val th  = new_type_definition(Tyop,EXISTS(mk_exists(v,mk_comb(P,v)),t) ax)
36 37
   val _   = if athy = tthy andalso rthy = tthy then () else
37  
-            raise ERR "define_tyop_in_thy" "wrong theory"
  38
+            raise ERR "define_tyop_in_thy" ("wrong theory: "^ct^" (given "^athy^" for "^abs^" and "^rthy^" for "^rep^")")
38 39
   val bij = define_new_type_bijections {name=Tyop^"_bij",ABS=abs,REP=rep,tyax=th}
39 40
   val [ar,ra] = CONJUNCTS bij
40 41
 in {rep_abs=SPEC_ALL ra,abs_rep=SPEC_ALL ar} end
41 42
 
42  
-fun define_const_in_thy ML_name {Thy,Name} rhs =
43  
-  if Thy = current_theory() then
  43
+fun define_const_in_thy ML_name {Thy,Name} rhs = let
  44
+  val ct = current_theory()
  45
+in
  46
+  if Thy = ct then
44 47
     new_definition ((ML_name Name)^"_def",mk_eq(mk_var(Name,type_of rhs),rhs))
45  
-  else raise ERR "define_const_in_thy" "wrong theory"
  48
+  else raise ERR "define_const_in_thy" ("wrong theory: "^ct^" (wanted "^Thy^" for "^Name^")")
  49
+end
46 50
 
47 51
 local
48 52
   open boolLib bossLib

0 notes on commit 9c4ab82

Please sign in to comment.
Something went wrong with that request. Please try again.