--- a/src/HOL/Metis_Examples/Type_Encodings.thy Tue Jul 26 18:11:38 2011 +0200
+++ b/src/HOL/Metis_Examples/Type_Encodings.thy Tue Jul 26 22:53:06 2011 +0200
@@ -26,45 +26,45 @@
tests. *)
val type_encs =
["erased",
- "poly_preds",
- "poly_preds_heavy",
+ "poly_guards",
+ "poly_guards_heavy",
"poly_tags",
"poly_tags_heavy",
"poly_args",
- "mono_preds",
- "mono_preds_heavy",
+ "mono_guards",
+ "mono_guards_heavy",
"mono_tags",
"mono_tags_heavy",
"mono_args",
- "mangled_preds",
- "mangled_preds_heavy",
+ "mangled_guards",
+ "mangled_guards_heavy",
"mangled_tags",
"mangled_tags_heavy",
"mangled_args",
"simple",
- "poly_preds?",
- "poly_preds_heavy?",
+ "poly_guards?",
+ "poly_guards_heavy?",
"poly_tags?",
(* "poly_tags_heavy?", *)
- "mono_preds?",
- "mono_preds_heavy?",
+ "mono_guards?",
+ "mono_guards_heavy?",
"mono_tags?",
"mono_tags_heavy?",
- "mangled_preds?",
- "mangled_preds_heavy?",
+ "mangled_guards?",
+ "mangled_guards_heavy?",
"mangled_tags?",
"mangled_tags_heavy?",
"simple?",
- "poly_preds!",
- "poly_preds_heavy!",
+ "poly_guards!",
+ "poly_guards_heavy!",
(* "poly_tags!", *)
"poly_tags_heavy!",
- "mono_preds!",
- "mono_preds_heavy!",
+ "mono_guards!",
+ "mono_guards_heavy!",
"mono_tags!",
"mono_tags_heavy!",
- "mangled_preds!",
- "mangled_preds_heavy!",
+ "mangled_guards!",
+ "mangled_guards_heavy!",
"mangled_tags!",
"mangled_tags_heavy!",
"simple!"]