55 |
55 |
56 (*Prints an exception, then fails*) |
56 (*Prints an exception, then fails*) |
57 fun print_sign_exn sign e = (print_sign_exn_unit sign e; raise e) |
57 fun print_sign_exn sign e = (print_sign_exn_unit sign e; raise e) |
58 |
58 |
59 val string_of_thm = PrintMode.setmp [] Display.string_of_thm_without_context; |
59 val string_of_thm = PrintMode.setmp [] Display.string_of_thm_without_context; |
60 val string_of_cterm = PrintMode.setmp [] Display.string_of_cterm; |
|
61 |
60 |
62 fun mk_meta_eq th = |
61 fun mk_meta_eq th = |
63 (case concl_of th of |
62 (case concl_of th of |
64 Const("Trueprop",_) $ (Const("op =",_) $ _ $ _) => th RS eq_reflection |
63 Const("Trueprop",_) $ (Const("op =",_) $ _ $ _) => th RS eq_reflection |
65 | Const("==",_) $ _ $ _ => th |
64 | Const("==",_) $ _ $ _ => th |
302 val _ = |
301 val _ = |
303 let |
302 let |
304 val lhs = #1 (Logic.dest_equals (prop_of (final init))) |
303 val lhs = #1 (Logic.dest_equals (prop_of (final init))) |
305 in |
304 in |
306 if not (lhs aconv origt) |
305 if not (lhs aconv origt) |
307 then (writeln "Something is utterly wrong: (orig,lhs,frozen type,t,tinst)"; |
306 then |
308 writeln (Display.string_of_cterm (cterm_of thy origt)); |
307 writeln (cat_lines |
309 writeln (Display.string_of_cterm (cterm_of thy lhs)); |
308 (["Something is utterly wrong: (orig, lhs, frozen type, t, tinst)", |
310 writeln (Display.string_of_cterm (cterm_of thy typet)); |
309 Syntax.string_of_term_global thy origt, |
311 writeln (Display.string_of_cterm (cterm_of thy t)); |
310 Syntax.string_of_term_global thy lhs, |
312 app (fn (n,T) => writeln (n ^ ": " ^ (Display.string_of_ctyp (ctyp_of thy T)))) Tinst; |
311 Syntax.string_of_term_global thy typet, |
313 writeln "done") |
312 Syntax.string_of_term_global thy t] @ |
|
313 map (fn (n, T) => n ^ ": " ^ Syntax.string_of_typ_global thy T) Tinst)) |
314 else () |
314 else () |
315 end |
315 end |
316 in |
316 in |
317 case t of |
317 case t of |
318 Const("all",_) $ (Abs(x,xT,Const("==",eqT) $ P $ Q)) => |
318 Const("all",_) $ (Abs(x,xT,Const("==",eqT) $ P $ Q)) => |
364 val _ = |
364 val _ = |
365 let |
365 let |
366 val lhs = #1 (Logic.dest_equals (prop_of (final init))) |
366 val lhs = #1 (Logic.dest_equals (prop_of (final init))) |
367 in |
367 in |
368 if not (lhs aconv origt) |
368 if not (lhs aconv origt) |
369 then (writeln "Something is utterly wrong: (orig,lhs,frozen type,t,tinst)"; |
369 then |
370 writeln (Display.string_of_cterm (cterm_of thy origt)); |
370 writeln (cat_lines |
371 writeln (Display.string_of_cterm (cterm_of thy lhs)); |
371 (["Something is utterly wrong: (orig, lhs, frozen type, t, tinst)", |
372 writeln (Display.string_of_cterm (cterm_of thy typet)); |
372 Syntax.string_of_term_global thy origt, |
373 writeln (Display.string_of_cterm (cterm_of thy t)); |
373 Syntax.string_of_term_global thy lhs, |
374 app (fn (n,T) => writeln (n ^ ": " ^ (Display.string_of_ctyp (ctyp_of thy T)))) Tinst; |
374 Syntax.string_of_term_global thy typet, |
375 writeln "done") |
375 Syntax.string_of_term_global thy t] @ |
|
376 map (fn (n, T) => n ^ ": " ^ Syntax.string_of_typ_global thy T) Tinst)) |
376 else () |
377 else () |
377 end |
378 end |
378 in |
379 in |
379 case t of |
380 case t of |
380 Const("==",T) $ P $ Q => |
381 Const("==",T) $ P $ Q => |
405 in |
406 in |
406 SOME res' |
407 SOME res' |
407 end |
408 end |
408 | _ => NONE) |
409 | _ => NONE) |
409 else NONE |
410 else NONE |
410 | _ => (error ("Bad eta_expand argument" ^ (string_of_cterm (cterm_of thy t))); NONE) |
411 | _ => error ("Bad eta_expand argument" ^ Syntax.string_of_term_global thy t) |
411 end |
412 end; |
412 handle e => (writeln "eta_expand internal error"; OldGoals.print_exn e) |
|
413 |
413 |
414 fun mk_tfree s = TFree("'"^s,[]) |
414 fun mk_tfree s = TFree("'"^s,[]) |
415 fun mk_free s t = Free (s,t) |
415 fun mk_free s t = Free (s,t) |
416 val xT = mk_tfree "a" |
416 val xT = mk_tfree "a" |
417 val yT = mk_tfree "b" |
417 val yT = mk_tfree "b" |