equal
deleted
inserted
replaced
233 val (assms_t, evals) = |
233 val (assms_t, evals) = |
234 assms_t :: evals |> merge_type_vars ? merge_type_vars_in_terms |
234 assms_t :: evals |> merge_type_vars ? merge_type_vars_in_terms |
235 |> pairf hd tl |
235 |> pairf hd tl |
236 val original_max_potential = max_potential |
236 val original_max_potential = max_potential |
237 val original_max_genuine = max_genuine |
237 val original_max_genuine = max_genuine |
238 (* |
|
239 val _ = print_g ("*** " ^ Syntax.string_of_term ctxt orig_t) |
|
240 val _ = List.app (fn t => print_g ("*** " ^ Syntax.string_of_term ctxt t)) |
|
241 orig_assm_ts |
|
242 *) |
|
243 val max_bisim_depth = fold Integer.max bisim_depths ~1 |
238 val max_bisim_depth = fold Integer.max bisim_depths ~1 |
244 val case_names = case_const_names thy stds |
239 val case_names = case_const_names thy stds |
245 val (defs, built_in_nondefs, user_nondefs) = all_axioms_of ctxt subst |
240 val (defs, built_in_nondefs, user_nondefs) = all_axioms_of ctxt subst |
246 val def_table = const_def_table ctxt subst defs |
241 val def_table = const_def_table ctxt subst defs |
247 val nondef_table = const_nondef_table (built_in_nondefs @ user_nondefs) |
242 val nondef_table = const_nondef_table (built_in_nondefs @ user_nondefs) |