411 end |
411 end |
412 |
412 |
413 | (_, Const _) => |
413 | (_, Const _) => |
414 let |
414 let |
415 val thy = ProofContext.theory_of ctxt |
415 val thy = ProofContext.theory_of ctxt |
416 fun matches_typ T T' = ( |
416 fun matches_typ T T' = |
417 let |
417 case (T, T') of |
418 val rty = #rtyp (quotdata_lookup_type thy T') |
418 (TFree _, TFree _) => true |
419 in |
419 | (TVar _, TVar _) => true |
420 if Sign.typ_instance thy (T, rty) then true else T = T' |
420 | (Type (s, tys), Type (s', tys')) => ( |
421 end |
421 (s = s' andalso tys = tys') orelse |
422 handle Not_found => (* raised by quotdata_lookup_type *) |
422 (* 'andalso' is buildin syntax so it needs to be expanded *) |
423 case (T, T') of |
423 (fold (fn x => fn y => x andalso y) (map2 matches_typ tys tys') (s = s') |
424 (TFree _, TFree _) => true |
424 handle UnequalLengths => false |
425 | (TVar _, TVar _) => true |
425 ) orelse |
426 | (Type (s, tys), Type (s', tys')) => |
426 let |
427 (* 'andalso' is buildin syntax so it needs to be expanded *) |
427 val rty = #rtyp (Quotient_Info.quotdata_lookup thy s') |
428 fold (fn x => fn y => x andalso y) (map2 matches_typ tys tys') (s = s') |
428 in |
429 handle UnequalLengths => false |
429 Sign.typ_instance thy (T, rty) |
430 ) |
430 end |
|
431 handle Not_found => false (* raised by quotdata_lookup *) |
|
432 ) |
|
433 | _ => false |
431 fun same_const (Const (s, T)) (Const (s', T')) = (s = s') andalso matches_typ T T' |
434 fun same_const (Const (s, T)) (Const (s', T')) = (s = s') andalso matches_typ T T' |
432 | same_const _ _ = false |
435 | same_const _ _ = false |
433 in |
436 in |
434 if same_const rtrm qtrm then rtrm |
437 if same_const rtrm qtrm then rtrm |
435 else |
438 else |