--- a/IntEx.thy	Fri Nov 27 02:45:54 2009 +0100
+++ b/IntEx.thy	Fri Nov 27 02:55:56 2009 +0100
@@ -212,7 +212,7 @@
 *}
 
 ML {* 
-mk_inj_REPABS_goal @{context} (reg_atrm, aqtrm) 
+inj_repabs_trm @{context} (reg_atrm, aqtrm) 
   |> Syntax.check_term @{context}
 *}
 
@@ -226,7 +226,7 @@
 done
 
 ML {*
-inj_REPABS @{context} (reg_atrm, aqtrm)  
+inj_repabs_trm @{context} (reg_atrm, aqtrm)  
 |> Syntax.string_of_term @{context}
 |> writeln
 *}